NSF.XGP[LET,JMC]1 - www.SailDart.org

perm filename NSF.XGP[LET,JMC]1 blob sn#537930 filedate 1980-09-29 generic text, type T, neo UTF8
/LMAR=0/XLINE=3/FONT#0=BAXL30/FONT#1=BAXM30/FONT#2=BAXB30/FONT#3=BAXS30/FONT#4=GACS25/FONT#5=CLAR30/FONT#8=SAIL25



␈↓ ↓H␈↓␈↓ ¬Research Proposal Submitted to


␈↓ ↓H␈↓␈↓ ∧∨␈↓αTHE NATIONAL SCIENCE FOUNDATION


␈↓ ↓H␈↓α␈↓ ε=␈↓for


␈↓ ↓H␈↓␈↓ ∧D␈↓αBasic Research in Arti␈↓␈↓βc␈↓␈↓αcial Intelligence


␈↓ ↓H␈↓α␈↓ ε@␈↓by


␈↓ ↓H␈↓␈↓ ¬iJohn McCarthy
␈↓ ↓H␈↓␈↓ ¬	Professor of Computer Science
␈↓ ↓H␈↓␈↓ ¬CPrincipal Investigator








␈↓ ↓H␈↓␈↓ ¬iSeptember 1980





␈↓ ↓H␈↓␈↓ ¬Computer Science Department

␈↓ ↓H␈↓␈↓ ¬∩␈↓αSTANFORD UNIVERSITY

␈↓ ↓H␈↓α␈↓ ¬M␈↓Stanford, California



␈↓ ↓H␈↓¬␈↓ ↓KResearch Proposal Submitted to the National Science Foundation





␈↓ ↓H␈↓Proposed Amount ␈↓&␈↓λ$423,225␈↓␈↓)αβ. Proposed E␈↓λ␈↓β@␈↓λ␈↓ective Date ␈↓&␈↓λ1 July 1981␈↓␈↓)αβ. Proposed Duration ␈↓&␈↓λ3 year␈↓␈↓)αβ



␈↓ ↓H␈↓Title ␈↓&␈↓λBasic Research in Artificial Intelligence␈↓␈↓)αβ



␈↓ ↓H␈↓Principal Investigator ␈↓&␈↓λJohn McCarthy␈↓␈↓)αβ␈↓ ε8Submitting Institution ␈↓&␈↓λStanford University␈↓␈↓)αβ
␈↓ ↓H␈↓  Soc. Sec. No. ␈↓&␈↓λ558-30-4793␈↓␈↓)αβ␈↓ ε8Department ␈↓&␈↓λ Computer Science    ␈↓␈↓)αβ
␈↓ ↓H␈↓␈↓ ε8Address ␈↓&␈↓λStanford, California 94305␈↓␈↓)αβ



␈↓ ↓H␈↓Make grant to ␈↓&␈↓λBoard of Trustees of the Leland Stanford Junior University␈↓␈↓)αβ



␈↓ ↓H␈↓Endorsements:

␈↓ ↓H␈↓␈↓ αXPrincipal Investigator␈↓ ¬hDepartment Head␈↓ λhInstitutional Admin. O␈↓λ␈↓β@␈↓λ␈↓icia

␈↓ ↓H␈↓Name␈↓ αX␈↓&␈↓λJohn McCarthy        ␈↓␈↓)αβ␈↓ ¬h␈↓&␈↓λEdward A. Feigenbaum ␈↓␈↓)αβ␈↓ λx␈↓&␈↓λ                    ␈↓␈↓)αβ


␈↓ ↓H␈↓Signature␈↓ αX␈↓&␈↓λ                     ␈↓␈↓)αβ␈↓ ¬h␈↓&␈↓λ                     ␈↓␈↓)αβ␈↓ λx␈↓&␈↓λ                    ␈↓␈↓)αβ

␈↓ ↓H␈↓Title␈↓ αX␈↓&␈↓λProfessor            ␈↓␈↓)αβ␈↓ ¬h␈↓&␈↓λProfessor & Chairman ␈↓␈↓)αβ␈↓ λx␈↓&␈↓λ                    ␈↓␈↓)αβ

␈↓ ↓H␈↓Telephone␈↓ αX␈↓&␈↓λ(415) 497-4430       ␈↓␈↓)αβ␈↓ ¬h␈↓&␈↓λ(415) 497-4079       ␈↓␈↓)αβ␈↓ λx␈↓&␈↓λ                    ␈↓␈↓)αβ

␈↓ ↓H␈↓Date␈↓ αX␈↓&␈↓λ                     ␈↓␈↓)αβ␈↓ ¬h␈↓&␈↓λ                     ␈↓␈↓)αβ␈↓ λx␈↓&␈↓λ                    ␈↓␈↓)αβ
␈↓ ↓H␈↓α␈↓ εP␈↓ L1


␈↓ ↓H␈↓α␈↓ βGAbstract                                  ␈↓ εh␈↓part␈α∂concerns␈α∂procedures␈α∂for␈α∂deciding␈α∂what␈α∞to
                                          ␈↓ εh␈↓do␈α⊃on␈α⊃the␈α⊃basis␈α⊃of␈α⊃the␈α⊃necessary␈α⊃facts.␈α⊂ Most
␈↓ ↓H␈↓        This␈α≤is␈α≤a␈α≤request␈α≤for␈α≤a␈α≥grant␈α≤for        ␈↓ εh␈↓work␈α→in␈α~AI␈α→has␈α→concerned␈α~␈↓↓heuristics␈↓,␈α→and
␈↓ ↓H␈↓continued␈αsupport␈α
of␈αbasic␈αresearch␈α
in␈αarti␈↓βC␈↓cial␈↓ εh␈↓computer␈α∩representations␈α⊃of␈α∩information␈α⊃have
␈↓ ↓H␈↓intelligence␈α⊂with␈α⊂emphasis␈α⊂on␈α⊂the␈α⊂structure␈α⊂of  ␈↓ εh␈↓been␈α∩chosen␈α∩that␈α⊃are␈α∩capable␈α∩of␈α⊃representing
␈↓ ↓H␈↓formal␈α∩reasoning,␈α∩epistemological␈α∪problems␈α∩of ␈↓ εh␈↓only␈α⊂a␈α∂part␈α⊂of␈α∂the␈α⊂information␈α∂that␈α⊂would␈α∂be
␈↓ ↓H␈↓arti␈↓βC␈↓cial␈α
intelligence␈α
and␈α
mathematical␈α
theory␈α
of␈↓ εh␈↓available␈αto␈αa␈αhuman.␈α The␈αmodes␈αof␈αreasoning
␈↓ ↓H␈↓computation.␈α≥ The␈α≥mathematical␈α≡theory␈α≥of      ␈↓ εh␈↓used␈α~by␈α~present␈α~programs␈α~are␈α≠often␈α~even
␈↓ ↓H␈↓computation␈α%supports␈α%the␈α%AI␈α&work␈α%by            ␈↓ εh␈↓weaker than the representations themselves.
␈↓ ↓H␈↓providing␈α∪tools␈α∀for␈α∪reasoning␈α∀about␈α∪complex
␈↓ ↓H␈↓strategies␈α∪and␈α∪showing␈α∩that␈α∪they␈α∪attain␈α∩their   ␈↓ εh␈↓        The␈α∞lines␈α∞of␈α∞research␈α∞we␈α∞plan␈α∞to␈α∞pursue
␈↓ ↓H␈↓goals.␈α
 The␈α
line␈αof␈α
research␈α
being␈α
pursued␈αwas   ␈↓ εh␈↓are␈α$exempli␈↓↓␈↓βC␈↓↓␈↓ed␈α$in␈α$the␈α$attached␈α#papers
␈↓ ↓H␈↓already␈αoutlined␈αin␈αour␈α1977␈αproposal,␈αand␈αthis  ␈↓ εh␈↓(McCarthy␈α∂1977a,b,c,d,␈α∞Moore␈α∂1977).␈α∂ Here␈α∞we
␈↓ ↓H␈↓proposal␈α∞incorporates␈α
much␈α∞material␈α∞from␈α
that  ␈↓ εh␈↓shall␈α
explain␈α
how␈α∞this␈α
work␈α
␈↓↓␈↓βC␈↓↓␈↓ts␈α∞together.␈α
 Our
␈↓ ↓H␈↓one.                                      ␈↓ εh␈↓long␈α∞range␈α∞goal␈α∞is␈α∞a␈α∞program␈α∞that␈α∞can␈α∞be␈α
told
                                          ␈↓ εh␈↓facts␈α~about␈α~the␈α~world␈α~and␈α~can␈α~use␈α~them
␈↓ ↓H␈↓α␈↓ ↓⎇Epistemological Problems of Arti␈↓␈↓βc␈↓␈↓αcial     ␈↓ εh␈↓e␈↓↓␈↓β@␈↓↓␈↓ectively␈α↔to␈α⊗achieve␈α↔the␈α⊗goals␈α↔it␈α↔is␈α⊗given.
␈↓ ↓H␈↓ β1␈↓αIntelligence                              ␈↓ εh␈↓Sometimes␈α
it␈αwill␈α
use␈α
the␈αfacts␈α
directly␈α
from␈αits
                                          ␈↓ εh␈↓data␈α≡base␈α≡using␈α≡deductive␈α≡and␈α≡inductive
␈↓ ↓H␈↓        Arti␈↓βC␈↓cial␈α∞intelligence␈α∞has␈α∞proved␈α∞to␈α∞be␈α∞a␈↓ εh␈↓processes␈α like␈α∨the␈α deductive␈α processes␈α∨of
␈↓ ↓H␈↓di␈↓β@␈↓icult␈α∨branch␈α≡of␈α∨science.␈α∨ Some␈α≡people       ␈↓ εh␈↓mathematical␈α∩logic.␈α⊃ However,␈α∩we␈α∩are␈α⊃already
␈↓ ↓H␈↓thought␈α
that␈α
human-level␈α
intelligence␈α∞could␈α
be ␈↓ εh␈↓sure,␈α$(McCarthy␈α$1977a),␈α$that␈α#conjectural
␈↓ ↓H␈↓achieved␈α⊂in␈α⊂ten␈α⊂or␈α⊂twenty␈α⊂years,␈α⊂but␈α⊂this␈α∂was     ␈↓ εh␈↓processes␈α≤will␈α≤be␈α≤needed␈α≤that␈α≥go␈α≤beyond
␈↓ ↓H␈↓based␈α⊃on␈α⊃the␈α⊃di␈↓β@␈↓iculties␈α⊃they␈α⊃could␈α⊃see␈α⊂when     ␈↓ εh␈↓deduction␈α
as␈α
presently␈α
conceived.␈α
 Sometimes␈αit
␈↓ ↓H␈↓they␈α→made␈α→the␈α→optimistic␈α→predictions.␈α→ Our     ␈↓ εh␈↓will␈α"use␈α!these␈α"facts␈α!to␈α"compile␈α!"expert
␈↓ ↓H␈↓opinion␈α∂is␈α∂that␈α∂major␈α∂scienti␈↓βC␈↓c␈α⊂discoveries␈α∂are ␈↓ εh␈↓programs"␈α→that␈α→use␈α_these␈α→facts␈α→in␈α→a␈α_more
␈↓ ↓H␈↓required␈α;before␈α;human-level␈α:general          ␈↓ εh␈↓e␈↓↓␈↓β@␈↓↓␈↓icient␈α∞way␈α∞than␈α∞simple␈α∂reasoning.␈α∞ However,
␈↓ ↓H␈↓intelligence␈αcan␈α
be␈αreached.␈α
 Moreover,␈αmany␈α
of ␈↓ εh␈↓the␈α↔expert␈α↔programs␈α⊗will␈α↔have␈α↔to␈α↔defer␈α⊗to
␈↓ ↓H␈↓these␈α∀discoveries␈α∪require␈α∀theoretical␈α∪advances␈↓ εh␈↓reasoning␈α∂when␈α⊂unexpected␈α∂use␈α∂of␈α⊂the␈α∂factual
␈↓ ↓H␈↓and␈α∃not␈α⊗merely␈α∃extending␈α∃current␈α⊗ideas␈α∃for      ␈↓ εh␈↓data-base is required.
␈↓ ↓H␈↓producing␈α⊂"expert␈α⊂programs"␈α⊂to␈α⊂new␈α⊂domains.
␈↓ ↓H␈↓The␈α↔recent␈α↔emphasis␈α↔by␈α↔ARPA␈α_and␈α↔other           ␈↓ εh␈↓        We␈α∞do␈α∞not␈α
propose␈α∞to␈α∞implement␈α∞such␈α
a
␈↓ ↓H␈↓agencies␈α∂sponsoring␈α∂AI␈α∂research␈α∂on␈α∞immediate   ␈↓ εh␈↓program␈αimmediately␈α-␈αmaybe␈αnot␈αat␈αall␈αwithin
␈↓ ↓H␈↓applications␈α
has␈α
resulted␈α
in␈α
a␈αserious␈α
imbalance.␈↓ εh␈↓the␈α
next␈α∞␈↓↓␈↓βC␈↓↓␈↓ve␈α
years.␈α
 This␈α∞is␈α
because␈α∞its␈α
success
␈↓ ↓H␈↓Deciding␈α⊂what␈α⊂the␈α⊂basic␈α⊂issues␈α⊂are␈α⊂is␈α∂di␈↓β@␈↓icult   ␈↓ εh␈↓depends␈α⊗on␈α∃successful␈α⊗formalization␈α⊗of␈α∃facts
␈↓ ↓H␈↓enough␈αwithout␈αhaving␈αto␈αformulate␈αeverything  ␈↓ εh␈↓about␈α⊂the␈α⊂world.␈α⊃ We␈α⊂have␈α⊂made␈α⊃progress␈α⊂in
␈↓ ↓H␈↓in␈α_terms␈α_of␈α_demonstration␈α_programs␈α→to␈α_be        ␈↓ εh␈↓this␈α
formalization,␈α
but␈α
we␈α
may␈α
be␈α
occupied␈α
with
␈↓ ↓H␈↓available␈α∂in␈α∂two␈α⊂years.␈α∂ While␈α∂there␈α⊂has␈α∂been    ␈↓ εh␈↓it␈α
exclusively␈αfor␈α
the␈αforseeable␈α
future.␈α In␈α
short
␈↓ ↓H␈↓some␈α∩recent␈α⊃increase␈α∩in␈α⊃understanding␈α∩of␈α⊃the    ␈↓ εh␈↓we␈α,will␈α+emphasize␈α,theoretical␈α+arti␈↓↓␈↓βC␈↓↓␈↓cial
␈↓ ↓H␈↓need␈αfor␈αbasic␈αresearch,␈αthe␈αmain␈αinterest␈αis␈α
still␈↓ εh␈↓intelligence␈α∀except␈α∪for␈α∀the␈α∪work␈α∀with␈α∪proof-
␈↓ ↓H␈↓on short term goals.                      ␈↓ εh␈↓checkers to be described below.

␈↓ ↓H␈↓        Our␈α∂research␈α∂is␈α⊂based␈α∂on␈α∂the␈α⊂idea␈α∂that,  ␈↓ εh␈↓        The␈α$main␈α#areas␈α$of␈α$our␈α#previous
␈↓ ↓H␈↓for␈α∩many␈α∪purposes,␈α∩the␈α∩problems␈α∪of␈α∩arti␈↓βC␈↓cial    ␈↓ εh␈↓accomplishment␈α≡and␈α≥future␈α≡work␈α≡are␈α≥the
␈↓ ↓H␈↓intelligence␈α
can␈α
be␈α
separated␈α
into␈α
two␈α
parts␈α
-␈α
an ␈↓ εh␈↓following (as now seen):
␈↓ ↓H␈↓epistemological␈α∞part␈α
and␈α∞a␈α
heuristic␈α∞part.␈α
 The
␈↓ ↓H␈↓␈↓↓epistemological␈↓␈α∃part␈α∃concerns␈α∃what␈α∃facts␈α∀and   ␈↓ εh␈↓1.␈αDevelopment␈αof␈α␈↓↓circumscription␈↓␈αas␈αa␈αmode␈αof
␈↓ ↓H␈↓inference␈α_rules␈α_are␈α_available␈α_for␈α_solving␈α_a     ␈↓ εh␈↓reasoning␈α≡and␈α≡its␈α≡application␈α∨to␈α≡arti␈↓↓␈↓βC␈↓↓␈↓cial
␈↓ ↓H␈↓problem␈α⊂and␈α⊂how␈α⊃they␈α⊂can␈α⊂be␈α⊃represented␈α⊂in       ␈↓ εh␈↓intelligence.␈α∨ ␈↓↓Circumscription␈↓␈α formalizes␈α∨the
␈↓ ↓H␈↓the␈α⊃memory␈α⊃of␈α⊂a␈α⊃computer,␈α⊃and␈α⊃the␈α⊂heuristic      ␈↓ εh␈↓process␈α∞of␈α∂concluding␈α∞(often␈α∞incorrectly)␈α∂that␈α∞a
␈↓ ↓H␈↓α␈↓ εP␈↓ J2


␈↓ ↓H␈↓certain␈αcollection␈αof␈αfacts␈αis␈αall␈αthat␈αare␈αrelevant␈↓ εh␈↓given␈α∃opportunities␈α∃to␈α∃observe␈α∃and␈α∃compute
␈↓ ↓H␈↓for␈αsolving␈αa␈αproblem.␈α It␈αdoes␈αthis␈αby␈αallowing  ␈↓ εh␈↓and act.
␈↓ ↓H␈↓one␈α∂to␈α∂formally␈α⊂assume␈α∂that␈α∂the␈α⊂entitities␈α∂that
␈↓ ↓H␈↓are␈α∞generated␈α∞by␈α
speci␈↓↓␈↓βC␈↓↓␈↓ed␈α∞processes␈α∞are␈α∞all␈α
the  ␈↓ εh␈↓α␈↓ εiRecent Advances and Changes in Direction of 
␈↓ ↓H␈↓entities␈αof␈αa␈αspeci␈↓↓␈↓βC␈↓↓␈↓ed␈αkind.␈α This␈αis␈α
common␈αin   ␈↓ εh␈↓ λK␈↓αthe Research 
␈↓ ↓H␈↓human␈α
reasoning␈αand,␈α
for␈αreasons␈α
described␈αin
␈↓ ↓H␈↓(McCarthy␈α∩1980),␈α∪cannot␈α∩be␈α∪accomplished␈α∩by     ␈↓ εh␈↓        Since␈α_our␈α_1977␈α_proposal,␈α_interest␈α↔has
␈↓ ↓H␈↓any form of deduction.                    ␈↓ εh␈↓increased␈α→in␈α→non-monotonic␈α→reasoning.␈α_ We
                                          ␈↓ εh␈↓organized␈α⊗a␈α↔mini-conference␈α⊗at␈α↔Stanford␈α⊗in
␈↓ ↓H␈↓2.␈αTreating␈αconcepts␈αas␈αobjects.␈α This,␈αdescribed␈↓ εh␈↓1978,␈αand␈αthat␈αled␈αto␈αa␈αspecial␈αissue␈αof␈α␈↓↓Arti␈↓␈↓βS␈↓␈↓↓cial
␈↓ ↓H␈↓in␈α∩(McCarthy␈α∩1977b),␈α∩facilitates,␈α∩and␈α∩may␈α⊃be    ␈↓ εh␈↓↓Intelligence␈↓␈α
containing␈α∞updated␈α
versions␈α∞of␈α
the
␈↓ ↓H␈↓required␈αfor,␈αreasoning␈αabout␈αknowledge,␈αbelief,␈↓ εh␈↓papers␈α∃presented␈α∃at␈α∃the␈α∃conference␈α∃togetther
␈↓ ↓H␈↓wants,␈α∪possibility␈α∪and␈α∪necessity.␈α∪ As␈α∪we␈α∩shall  ␈↓ εh␈↓with␈αa␈αpaper␈αby␈αRaymond␈αReiter␈α(1980).␈α Drew
␈↓ ↓H␈↓explain␈αlater,␈αit␈αmay␈αbe␈αnecessary␈αto␈αreplace␈αthe ␈↓ εh␈↓McDermott␈α⊃and␈α⊃Jon␈α⊂Doyle␈α⊃have␈α⊃attacked␈α⊂the
␈↓ ↓H␈↓approach␈α⊃of␈α⊃that␈α⊃paper␈α⊃by␈α⊃one␈α⊃which␈α⊃makes        ␈↓ εh␈↓problem␈α∞through␈α
what␈α∞they␈α∞call␈α
␈↓↓non-monotonic
␈↓ ↓H␈↓distinctions␈α∀of␈α∪language␈α∀between␈α∀objects␈α∪and   ␈↓ εh␈↓↓logic␈↓␈α∀and␈α∀Raymond␈α∀Reiter␈α∀has␈α∀introduced␈α∪a
␈↓ ↓H␈↓and␈αconcepts␈αof␈αthem␈αonly␈αwhen␈αrequired.␈α Not    ␈↓ εh␈↓␈↓↓logic␈α∂of␈α∂defaults␈↓.␈α∂ Our␈α∂own␈α⊂approach␈α∂through
␈↓ ↓H␈↓making␈α
the␈α
distinctions␈α
would␈α
be␈αaccomplished  ␈↓ εh␈↓circumscription␈α∂has␈α∂been␈α∂further␈α∂developed␈α∂in
␈↓ ↓H␈↓by some kind of non-monotonic reasoning.  ␈↓ εh␈↓the published version

␈↓ ↓H␈↓3.␈α≥The␈α≡current␈α≥biggest␈α≥gap␈α≡in␈α≥computer          ␈↓ εh␈↓        Participation␈α∃in␈α∃the␈α∃study␈α⊗on␈α∃arti␈↓↓␈↓βC␈↓↓␈↓cial
␈↓ ↓H␈↓reasoning␈α→about␈α→the␈α→physical␈α→world␈α→is␈α→the       ␈↓ εh␈↓intelligence␈α
and␈α∞philosophy␈α
held␈α
in␈α∞1979-80␈α
at
␈↓ ↓H␈↓complete␈α⊃lack␈α⊃of␈α⊃a␈α⊃system␈α⊃for␈α∩reasoning␈α⊃with     ␈↓ εh␈↓the␈α∞Center␈α∞for␈α∞Advanced␈α∞Study␈α∞in␈α∞Behavioral
␈↓ ↓H␈↓partial␈α∞information␈α∞about␈α∞concurrent␈α∞processes.␈↓ εh␈↓Sciences␈α∂has␈α∂produced␈α∞somewhat␈α∂of␈α∂change␈α∞in
␈↓ ↓H␈↓All␈α≠the␈α~current␈α≠problem␈α≠solving␈α~programs       ␈↓ εh␈↓viewpoint␈α
although␈αnot␈α
yet␈αto␈α
de␈↓↓␈↓βC␈↓↓␈↓nite␈αtechnical
␈↓ ↓H␈↓assume␈α≥that␈α≤each␈α≥action␈α≤of␈α≥the␈α≤program          ␈↓ εh␈↓results.  Consider the following problem:
␈↓ ↓H␈↓produces␈α⊗a␈α⊗next␈α⊗state␈α⊗that␈α⊗depends␈α⊗on␈α⊗the
␈↓ ↓H␈↓current␈α⊃state,␈α⊃the␈α∩action,␈α⊃and␈α⊃sometimes␈α∩on␈α⊃a    ␈↓ εh␈↓        ␈↓↓Suppose␈α∞that␈α∞a␈α∞law␈α
making␈α∞it␈α∞a␈α∞crime␈α
to
␈↓ ↓H␈↓random␈αvariable.␈α They␈αdon't␈αtake␈αinto␈αaccount  ␈↓ εh␈↓↓"attempt␈α↔to␈α↔bribe␈α↔a␈α↔public␈α↔o␈↓␈↓βP␈↓␈↓↓icial"␈α↔has␈α⊗been
␈↓ ↓H␈↓continuous␈α↔processes␈α↔or␈α↔the␈α↔fact␈α↔that␈α↔other     ␈↓ εh␈↓↓passed,␈α∂and␈α∂suppose␈α∂further␈α∂that␈α∂the␈α⊂law␈α∂has
␈↓ ↓H␈↓actions␈α⊃and␈α⊃events␈α⊃may␈α⊃be␈α⊃taking␈α⊃place.␈α⊂ We      ␈↓ εh␈↓↓been␈α∃enforced␈α∀with␈α∃various␈α∃trials,␈α∀convictions
␈↓ ↓H␈↓believe␈α∂that␈α∂circumscription␈α∂may␈α⊂be␈α∂important  ␈↓ εh␈↓↓and␈α⊃appeals␈α⊃for␈α∩20␈α⊃years␈α⊃before␈α∩the␈α⊃following
␈↓ ↓H␈↓in␈α⊃formalizing␈α∩what␈α⊃people␈α⊃know␈α∩about␈α⊃such      ␈↓ εh␈↓↓questions arise.
␈↓ ↓H␈↓processes.␈α∪ Little␈α∪progress␈α∪has␈α∪been␈α∀made␈α∪by
␈↓ ↓H␈↓anyone on this problem in the last few years.␈↓ εh␈↓↓        (1)␈α∂Person␈α∂A␈α∂attempts␈α∂to␈α∂bribe␈α∂B␈α∂to␈α∞help
                                          ␈↓ εh␈↓↓him␈α∞get␈α
a␈α∞contract␈α
under␈α∞the␈α
impression␈α∞that␈α
B
␈↓ ↓H␈↓4.␈α⊃We␈α⊂also␈α⊃plan␈α⊂some␈α⊃study␈α⊂of␈α⊃the␈α⊃theory␈α⊂of        ␈↓ εh␈↓↓is␈α
a␈α
private␈α
consultant␈α
to␈α
a␈α
government␈αagency.
␈↓ ↓H␈↓patterns,␈α⊗especially␈α↔higher␈α⊗order␈α↔patterns␈α⊗in  ␈↓ εh␈↓↓In␈α
fact,␈α
B␈αis␈α
an␈α
o␈↓␈↓βP␈↓␈↓↓icial␈αof␈α
the␈α
agency.␈α
 A␈αo␈↓␈↓βP␈↓␈↓↓ers
␈↓ ↓H␈↓which␈α∞function␈α∞variables␈α
may␈α∞be␈α∞matched␈α
and     ␈↓ εh␈↓↓the␈α∞defense␈α∞that␈α∞since␈α∞he␈α∞didn't␈α∞know␈α∞B␈α∞was␈α
a
␈↓ ↓H␈↓relations␈α⊃between␈α∩patterns␈α⊃-␈α⊃for␈α∩example,␈α⊃the   ␈↓ εh␈↓↓public␈αo␈↓␈↓βP␈↓␈↓↓icial,␈αhe␈αcouldn't␈αhave␈αbeen␈αattempting
␈↓ ↓H␈↓relation␈α
between␈α
a␈α
pattern␈α
describing␈α
a␈α
type␈αof  ␈↓ εh␈↓↓to bribe a public o␈↓␈↓βP␈↓␈↓↓icial.
␈↓ ↓H␈↓three-dimensional␈αobject␈α
such␈αas␈α
a␈αperson␈α
or␈αa
␈↓ ↓H␈↓vehicle␈αand␈αits␈αpatterns␈αof␈αits␈αperception␈α-␈αsuch ␈↓ εh␈↓↓        (2)␈α∪C␈α∀attempts␈α∪to␈α∪bribe␈α∀D,␈α∪but␈α∀D␈α∪had
␈↓ ↓H␈↓as␈α∪its␈α∪projection␈α∪on␈α∩a␈α∪retina␈α∪as␈α∪modi␈↓↓␈↓βC␈↓↓␈↓ed␈α∩by       ␈↓ εh␈↓↓resigned␈α⊂his␈α⊂position␈α⊂as␈α⊂a␈α⊂public␈α⊃o␈↓␈↓βP␈↓␈↓↓icial␈α⊂before
␈↓ ↓H␈↓angle␈αof␈αvision,␈αlighting␈αand␈αocclusion␈αby␈αother ␈↓ εh␈↓↓the␈α⊂attempt␈α⊂was␈α⊂made.␈α⊂ The␈α⊂defense␈α⊃is␈α⊂o␈↓␈↓βP␈↓␈↓↓ered
␈↓ ↓H␈↓objects.                                  ␈↓ εh␈↓↓that␈α∞attempting␈α∞to␈α∞bribe␈α∞someone␈α∞who␈α∞in␈α∂fact␈α∞is
                                          ␈↓ εh␈↓↓not␈α∂a␈α∂public␈α∂o␈↓␈↓βP␈↓␈↓↓icial␈α∂isn't␈α∂attempting␈α∂to␈α⊂bribe␈α∂a
␈↓ ↓H␈↓        In␈α↔all␈α⊗this␈α↔work,␈α⊗the␈α↔emphasis␈α↔is␈α⊗on     ␈↓ εh␈↓↓public o␈↓␈↓βP␈↓␈↓↓icial.
␈↓ ↓H␈↓representation␈α≡of␈α∨the␈α≡information␈α∨that␈α≡is
␈↓ ↓H␈↓actually␈α∪available␈α∪to␈α∪a␈α∪person␈α∪or␈α∪robot␈α∪with     ␈↓ εh␈↓↓        (3)␈αE␈α
lets␈αit␈α
be␈αknown␈α
around␈αtown␈αthat␈α
he
␈↓ ↓H␈↓α␈↓ εP␈↓ J3


␈↓ ↓H␈↓↓will␈αpay␈α$1,000␈αto␈αany␈αpublic␈αo␈↓␈↓βP␈↓␈↓↓icial␈αwho␈αcan␈α␈↓␈↓βS␈↓␈↓↓x   ␈↓ εh␈↓have␈α↔di␈↓↓␈↓β@␈↓↓␈↓erent␈α⊗forms,␈α↔and␈α⊗if␈α↔the␈α⊗legislature
␈↓ ↓H␈↓↓his␈αdrunk␈αdriving␈αconviction.␈α There␈αhappens␈αto ␈↓ εh␈↓wrote␈α∩the␈α⊃law␈α∩in␈α⊃the␈α∩language␈α∩of␈α⊃(McCarthy
␈↓ ↓H␈↓↓be␈α⊂no␈α⊂o␈↓␈↓βP␈↓␈↓↓icial␈α⊂who␈α⊃can␈α⊂␈↓␈↓βS␈↓␈↓↓x␈α⊂the␈α⊂conviction.␈α⊃ Is␈α⊂E     ␈↓ εh␈↓xxx),␈α∂they␈α∂would␈α∂automatically␈α∂say␈α∂one␈α∂or␈α∞the
␈↓ ↓H␈↓↓guilty␈α∂of␈α∞attempting␈α∂to␈α∂bribe␈α∞a␈α∂public␈α∂o␈↓␈↓βP␈↓␈↓↓icial␈α∞if ␈↓ εh␈↓other␈α∀or␈α∃the␈α∀conjunction␈α∀or␈α∃the␈α∀disjunction.
␈↓ ↓H␈↓↓he␈αisn't␈αattempting␈αto␈αbribe␈αa␈αspeci␈↓␈↓βS␈↓␈↓↓c␈αperson?␈α Is␈↓ εh␈↓However,␈α⊂it␈α⊂now␈α⊂seems␈α⊂that␈α⊂philosophers␈α∂and
␈↓ ↓H␈↓↓it␈αrelevant␈αwhether␈αthere␈αis␈αa␈αperson␈αwho␈αcan␈αdo   ␈↓ εh␈↓lawyers␈α
invent␈α
new␈α
distinctions␈α
all␈α
the␈αtime,␈α
and
␈↓ ↓H␈↓↓what E wants done␈↓?                        ␈↓ εh␈↓we␈α∞certainly␈α
can't␈α∞revise␈α
the␈α∞foundation␈α∞of␈α
our
                                          ␈↓ εh␈↓language␈α⊃every␈α⊃time␈α⊃such␈α⊃a␈α∩distinction␈α⊃comes
␈↓ ↓H␈↓        Such␈α≠questions␈α≠are␈α≠familiar␈α≠to␈α≠both    ␈↓ εh␈↓along.␈α∃ Even␈α∃if␈α⊗we␈α∃could,␈α∃the␈α⊗question␈α∃still
␈↓ ↓H␈↓philosophers␈α≤and␈α≤lawyers.␈α≥ The␈α≤distinction    ␈↓ εh␈↓arises␈α⊂of␈α⊃what␈α⊂was␈α⊂the␈α⊃meaning␈α⊂of␈α⊃what␈α⊂was
␈↓ ↓H␈↓between␈α
(1)␈α
and␈α
(2)␈α
is␈αthe␈α
well␈α
known␈α
␈↓↓de␈α
re␈α-␈α
de     ␈↓ εh␈↓said before the distinction was made.
␈↓ ↓H␈↓↓dicto␈↓␈α≥distinction␈α≥between␈α≥interpretations␈α≥of
␈↓ ↓H␈↓"attempting␈α∪to␈α∪bribe␈α∪a␈α∪public␈α∀o␈↓↓␈↓β@␈↓↓␈↓icial".␈α∪ This   ␈↓ εh␈↓        While␈αit␈αis␈αpossible␈αthat␈αthe␈αformalism␈αof
␈↓ ↓H␈↓distinction␈α*and␈α)even␈α*more␈α)complicated         ␈↓ εh␈↓(McCarthy␈α≤xxx)␈α≤could␈α≤cover␈α≤all␈α≤cases␈α≠of
␈↓ ↓H␈↓distinctions␈α
have␈α
been␈αmade␈α
in␈α
court␈αdecisions. ␈↓ εh␈↓interest,␈α↔this␈α⊗now␈α↔seems␈α⊗unlikely,␈α↔and␈α↔it␈α⊗is
␈↓ ↓H␈↓A␈αfamous␈α
1879␈αcase␈αconcerns␈α
a␈αcow␈α
which␈αwas       ␈↓ εh␈↓interesting␈α_to␈α_explore␈α_a␈α→di␈↓↓␈↓β@␈↓↓␈↓erent␈α_approach.
␈↓ ↓H␈↓bought␈α
on␈αthe␈α
basis␈α
that␈αthe␈α
seller␈α
thought␈αthe   ␈↓ εh␈↓This␈α∩new␈α∪approach␈α∩has␈α∩other␈α∪advantages␈α∩as
␈↓ ↓H␈↓cow␈α∪was␈α∪infertile␈α∪and␈α∪the␈α∪buyer␈α∀thought␈α∪he       ␈↓ εh␈↓well.␈α∀ The␈α∀idea␈α∀is␈α∀complicated␈α∀and␈α∀not␈α∪well
␈↓ ↓H␈↓could␈α"make␈α!the␈α"cow␈α!breed.␈α" When␈α!he              ␈↓ εh␈↓developed, but here is the basic idea.
␈↓ ↓H␈↓discovered␈α∞that␈α∞the␈α∞cow␈α∞was␈α∞actually␈α
pregnant,
␈↓ ↓H␈↓the␈αseller␈α
refused␈αto␈αdeliver␈α
on␈αthe␈αgrounds␈α
that ␈↓ εh␈↓        We␈α∂still␈α∂use␈α∂a␈α∞␈↓↓␈↓βC␈↓↓␈↓rst␈α∂order␈α∂system,␈α∂but␈α∞we
␈↓ ↓H␈↓he␈α_had␈α_sold␈α_a␈α_barren␈α_cow.␈α_ The␈α_issue␈α_is           ␈↓ εh␈↓have␈α∂only␈α∞one␈α∂form␈α∞expression.␈α∂ We␈α∂have␈α∞the
␈↓ ↓H␈↓whether there was a meeting of minds.     ␈↓ εh␈↓default␈α
rule␈α
that␈α
equals␈α
may␈α
be␈α∞substituted␈α
for
                                          ␈↓ εh␈↓equals␈α∩unless␈α∩there␈α∩is␈α∩a␈α∩reason␈α∩why␈α∪not.␈α∩ In
␈↓ ↓H␈↓        When␈αwe␈αtry␈αto␈αdesign␈αan␈αAI␈αsystem,␈αour   ␈↓ εh␈↓philosopher's␈α
Latin␈α
␈↓↓Ceteris␈α
paribus,␈α
de␈α
re␈α
=␈αde
␈↓ ↓H␈↓interest␈α
in␈α
such␈αproblems␈α
is␈α
di␈↓↓␈↓β@␈↓↓␈↓erent␈α
from␈αthat  ␈↓ εh␈↓↓dicto␈↓.␈α≥ Our␈α≤hope␈α≥is␈α≤that␈α≥extending␈α≤non-
␈↓ ↓H␈↓expressed␈α∃by␈α∃either␈α∃philosophers␈α∃or␈α∀lawyers.   ␈↓ εh␈↓monotonic␈α!reasoning␈α!to␈α!say␈α!that␈α!certain
␈↓ ↓H␈↓They␈α
are␈αinterested␈α
in␈αmaking␈α
distinctions␈αthat ␈↓ εh␈↓concepts␈α↔are␈α⊗not␈α↔ambiguous␈α⊗unless␈α↔there␈α⊗is
␈↓ ↓H␈↓have␈α∞not␈α∞previously␈α∞been␈α∞made.␈α∂ The␈α∞primary     ␈↓ εh␈↓reason␈α∪to␈α∩the␈α∪contrary␈α∩will␈α∪allow␈α∪AI␈α∩systems
␈↓ ↓H␈↓AI␈α∂interest␈α⊂should␈α∂be␈α∂in␈α⊂the␈α∂state␈α∂of␈α⊂mind␈α∂of      ␈↓ εh␈↓that behave more like people in that respect.
␈↓ ↓H␈↓the␈α≥lawyer␈α≥or␈α≡judge␈α≥who␈α≥tries␈α≡cases␈α≥of
␈↓ ↓H␈↓attempting␈α
to␈α
bribe␈α∞a␈α
public␈α
o␈↓↓␈↓β@␈↓↓␈↓icial␈α∞for␈α
twenty  ␈↓ εh␈↓        The␈α↔philosophers␈α↔have␈α↔a␈α_slogan␈α↔that
␈↓ ↓H␈↓years␈α∂without␈α∂ever␈α∂thinking␈α∂of␈α∂the␈α∂distinction. ␈↓ εh␈↓doing␈α∞philosophy␈α∞should␈α∞not␈α∞depend␈α∞on␈α
doing
␈↓ ↓H␈↓When␈α∪the␈α∪distinction␈α∪is␈α∪pointed␈α∪out,␈α∪he␈α∩can      ␈↓ εh␈↓all␈α→science␈α→␈↓↓␈↓βC␈↓↓␈↓rst.␈α→ Thus␈α→understanding␈α→what
␈↓ ↓H␈↓understand␈αthat␈αthere␈αis␈αa␈α
distinction,␈αalthough␈↓ εh␈↓people␈α∀mean␈α∃by␈α∀the␈α∃word␈α∀"␈↓↓␈↓βC␈↓↓␈↓sh"␈α∃should␈α∀not
␈↓ ↓H␈↓he␈α
may␈α
not␈α
have␈α
any␈α
de␈↓↓␈↓βC␈↓↓␈↓nite␈α
way␈α
of␈α
resolving      ␈↓ εh␈↓depend␈α~on␈α≠the␈α~philosopher␈α≠knowing␈α~what
␈↓ ↓H␈↓the ambiguity in the law.                 ␈↓ εh␈↓distinguishes␈α⊗␈↓↓␈↓βC␈↓↓␈↓sh␈α∃from␈α⊗other␈α⊗vertebrates.␈α∃ It
                                          ␈↓ εh␈↓appears␈α∪that␈α∪we␈α∀need␈α∪another␈α∪slogan␈α∀to␈α∪the
␈↓ ↓H␈↓        (McCarthy␈α_xxx)␈α_presents␈α→a␈α_formalism   ␈↓ εh␈↓e␈↓↓␈↓β@␈↓↓␈↓ect␈α∃that␈α∃doing␈α∃AI␈α∃should␈α∃not␈α∃depend␈α∃on
␈↓ ↓H␈↓that␈α∂resolves␈α∂simple␈α∂forms␈α∂of␈α∂␈↓↓de␈α∂re␈α∂-␈α⊂de␈α∂dicto␈↓     ␈↓ εh␈↓doing␈α⊂all␈α⊂philosophy␈α⊂␈↓↓␈↓βC␈↓↓␈↓rst.␈α⊂ Thus␈α⊂it␈α⊂should␈α⊂be
␈↓ ↓H␈↓distinction,␈α
and␈α
we␈αknew␈α
about␈α
the␈α
problem␈αof    ␈↓ εh␈↓possible␈αto␈αdesign␈αa␈αprogram␈αthat␈αcould␈αdiscuss
␈↓ ↓H␈↓stating␈α∞that␈α∞John␈α∞is␈α∞seeking␈α∞a␈α∞unicorn␈α
without   ␈↓ εh␈↓cases␈α∩of␈α∩attempting␈α∩to␈α∩bribe␈α∩a␈α∩public␈α∩o␈↓↓␈↓β@␈↓↓␈↓icial
␈↓ ↓H␈↓presuming␈α≡the␈α≡existence␈α≡of␈α≡unicorns␈α≡and        ␈↓ εh␈↓without␈α∃the␈α∃programmer␈α∃knowing␈α∃about␈α∀the
␈↓ ↓H␈↓planned␈α⊂to␈α⊂resolve␈α⊂it.␈α⊂ The␈α⊂formalism␈α⊃of␈α⊂that    ␈↓ εh␈↓ambiguous␈αcases.␈α
 The␈αprogram␈αhe␈α
creates,␈αlike
␈↓ ↓H␈↓paper␈α≡allowed␈α≡both␈α≡physical␈α∨entities␈α≡and       ␈↓ εh␈↓the␈α⊗programmer␈α⊗himself,␈α⊗should␈α⊗be␈α⊗able␈α⊗to
␈↓ ↓H␈↓concepts␈α∩of␈α⊃them␈α∩to␈α⊃be␈α∩individuals␈α⊃in␈α∩a␈α⊃␈↓↓␈↓βC␈↓↓␈↓rst      ␈↓ εh␈↓understand␈α⊃the␈α⊃distinction␈α⊃when␈α⊃it␈α⊃is␈α⊂pointed
␈↓ ↓H␈↓order␈α∃theory.␈α∃ All␈α∀statements␈α∃of␈α∃knowing␈α∀or     ␈↓ εh␈↓out,␈α
but␈α
it␈α
shouldn't␈αhave␈α
an␈α
automatic␈α
way␈αof
␈↓ ↓H␈↓wanting␈α
or␈α
attempting␈α
take␈α
concepts␈α
of␈α
objects, ␈↓ εh␈↓resolving the doubtful cases.
␈↓ ↓H␈↓and␈α≠the␈α≠␈↓↓de␈α≠re␈↓␈α≠and␈α≠␈↓↓de␈α≠dicto␈↓␈α≤versions␈α≠of
␈↓ ↓H␈↓"attempting␈α∪to␈α∪bribe␈α∪a␈α∪public␈α∪o␈↓↓␈↓β@␈↓↓␈↓icial"␈α∪would    ␈↓ εh␈↓        We␈α have␈α some␈α examples␈α!of␈α using
␈↓ ↓H␈↓α␈↓ εP␈↓ G4


␈↓ ↓H␈↓circumscription␈α→for␈α_this␈α→in␈α_a␈α→second␈α_order      ␈↓ εh␈↓a␈α!system,␈α he␈α!establishes␈α!shortcuts␈α whose
␈↓ ↓H␈↓formalism.␈α⊂ Namely,␈α⊂a␈α⊂suitable␈α⊂circumscription␈↓ εh␈↓repeated use keeps down the length of a proof.
␈↓ ↓H␈↓formula␈αasserts␈αthat␈αa␈αfunction␈αlike␈α⊗Telephone
␈↓ ↓H␈↓of␈α
(McCarthy␈α
xxx)␈αis␈α
extensional␈α
unless␈αthere␈α
is ␈↓ εh␈↓        When␈α≡we␈α≥turn␈α≡to␈α≥non-mathematical
␈↓ ↓H␈↓a␈αreason␈αwhy␈αnot.␈α However,␈αthis␈αis␈αmay␈αnot␈αbe     ␈↓ εh␈↓reasoning,␈αpresent␈α
logical␈αsystems␈α
are␈αeven␈α
more
␈↓ ↓H␈↓a␈α≠su␈↓↓␈↓β@␈↓↓␈↓iciently␈α≤general␈α≠way␈α≠of␈α≤treating␈α≠the       ␈↓ εh␈↓inadequate␈α
for␈α
expressing␈α
the␈α
reasoning␈αused␈α
in
␈↓ ↓H␈↓problem.                                  ␈↓ εh␈↓solving␈α⊂problems.␈α⊂ We␈α⊂have␈α⊂already␈α∂identi␈↓↓␈↓βC␈↓↓␈↓ed
                                          ␈↓ εh␈↓two␈α&such␈α&inadequacies:␈α&problem␈α&solving
␈↓ ↓H␈↓        McCarthy␈α↔and␈α↔interested␈α↔students␈α⊗will ␈↓ εh␈↓requires␈α∞that␈α∞conventional␈α∂deductive␈α∞reasoning
␈↓ ↓H␈↓explore this problem in the next three years.␈↓ εh␈↓interact␈α⊃with␈α⊃observation␈α⊃and␈α⊃use␈α⊂computable
                                          ␈↓ εh␈↓models,␈αand␈αcircumscription␈αas␈αdescribed␈αabove
␈↓ ↓H␈↓α␈↓ α8Proof-Checking by Computer                ␈↓ εh␈↓and␈α⊃in␈α⊃(McCarthy␈α⊂1977a),␈α⊃requires␈α⊃new␈α⊂tools.
                                          ␈↓ εh␈↓The␈α
proof-checker␈α∞allows␈α
us␈α
to␈α∞verify␈α
whether
␈↓ ↓H␈↓        Computer␈α∩proof-checking␈α∩is␈α∩needed␈α⊃for ␈↓ εh␈↓our␈αaxioms␈αand␈αconventional␈αrules␈αof␈αinference
␈↓ ↓H␈↓the␈α
AI␈α
research,␈α
and␈α
its␈α
applications␈αto␈α
program ␈↓ εh␈↓together␈α⊃with␈α∩our␈α⊃proposed␈α⊃new␈α∩methods␈α⊃are
␈↓ ↓H␈↓veri␈↓↓␈↓βC␈↓↓␈↓cation␈α∩will␈α∪become␈α∩practical␈α∩in␈α∪the␈α∩very   ␈↓ εh␈↓really␈α∨adequate␈α∨to␈α∨express␈α the␈α∨reasoning
␈↓ ↓H␈↓near␈α∀future,␈α∪but␈α∀␈↓↓␈↓βC␈↓↓␈↓rst␈α∪we␈α∀must␈α∀distinguish␈α∪it     ␈↓ εh␈↓required to solve a problem.
␈↓ ↓H␈↓from theorem proving by computer.
                                          ␈↓ εh␈↓        We␈α∃have␈α∃a␈α∃proof-checker␈α∃called␈α∃FOL
␈↓ ↓H␈↓        It␈α⊃is␈α∩an␈α⊃essential␈α⊃part␈α∩of␈α⊃the␈α∩notion␈α⊃of  ␈↓ εh␈↓(for␈α∩␈↓↓␈↓βC␈↓↓␈↓rst␈α∪order␈α∩logic)␈α∩(Weyhrauch␈α∪1977a),␈α∩we
␈↓ ↓H␈↓proof␈αin␈αa␈αformal␈α
system␈αthat␈αa␈αcandidate␈α
proof   ␈↓ εh␈↓have␈α∀been␈α∪improving␈α∀it␈α∪since␈α∀1973,␈α∀and␈α∪we
␈↓ ↓H␈↓can␈αbe␈αchecked␈αby␈αa␈αmechanical␈αprocess.␈α It␈αis␈α
a   ␈↓ εh␈↓propose␈αto␈αimprove␈α
it␈αfurther␈αunder␈α
this␈αgrant.
␈↓ ↓H␈↓consequence␈α∪of␈α∀the␈α∪work␈α∪of␈α∀Goedel,␈α∪Church       ␈↓ εh␈↓(Rewriting␈α⊂it␈α∂from␈α⊂scratch␈α∂will␈α⊂be␈α⊂required␈α∂at
␈↓ ↓H␈↓and␈α∀Turing␈α∀that␈α∀no␈α∀mechanical␈α∃process␈α∀can       ␈↓ εh␈↓some␈α
point,␈αbut␈α
we␈αaren't␈α
sure␈αwhen␈α
this␈αwill␈α
be
␈↓ ↓H␈↓always␈α⊂determine␈α⊂whether␈α⊂a␈α⊂proof␈α⊂of␈α⊂a␈α⊂given      ␈↓ εh␈↓the␈αbest␈αuse␈αof␈αlimited␈αmanpower).␈α With␈αFOL,
␈↓ ↓H␈↓sentence␈αexists␈αin␈αa␈αformal␈αsystem.␈α In␈αprinciple,␈↓ εh␈↓we␈α∃have␈α∃checked␈α∃a␈α∃variety␈α∃of␈α∀mathematical
␈↓ ↓H␈↓therefore,␈αproof-checking␈α
should␈αbe␈α
easy,␈αwhile␈↓ εh␈↓proofs,␈α↔and␈α↔each␈α↔such␈α↔project␈α↔has␈α_told␈α↔us
␈↓ ↓H␈↓all␈αthe␈αdi␈↓↓␈↓β@␈↓↓␈↓iculties␈αof␈αunderstanding␈αthe␈αcreative␈↓ εh␈↓something␈α∪about␈α∩how␈α∪to␈α∩improve␈α∪the␈α∩proof-
␈↓ ↓H␈↓processes␈α⊃of␈α⊃a␈α⊂mathematician␈α⊃are␈α⊃involved␈α⊂in    ␈↓ εh␈↓checker␈α$or␈α$how␈α$to␈α$formalize␈α%a␈α$given
␈↓ ↓H␈↓making a high powered theorem prover.     ␈↓ εh␈↓mathematical␈α↔domain␈α↔or␈α↔how␈α↔to␈α↔write␈α↔and
                                          ␈↓ εh␈↓debug␈α
proofs.␈α
 The␈α
proofs␈α
described␈α
below␈α
each
␈↓ ↓H␈↓        However,␈α∃in␈α∀spite␈α∃of␈α∀the␈α∃simplicity␈α∀of  ␈↓ εh␈↓tested␈α#the␈α#adequacy␈α#of␈α#FOL␈α#and␈α"our
␈↓ ↓H␈↓modern␈α
logical␈α
and␈α
set␈α
theoretic␈α
systems␈α
and␈α
the ␈↓ εh␈↓axiomatizations.
␈↓ ↓H␈↓brevity␈α∪with␈α∩which␈α∪they␈α∪permit␈α∩axiomatizing
␈↓ ↓H␈↓mathematical␈α⊗and␈α⊗physical␈α↔systems,␈α⊗checking   ␈↓ εh␈↓(a)␈α∀Any␈α∀device␈α∀capable␈α∀of␈α∀accepting␈α∀general
␈↓ ↓H␈↓actual␈α proofs␈α has␈α encountered␈α∨formidable      ␈↓ εh␈↓mathematical␈α∂reasoning␈α∞must␈α∂be␈α∞able␈α∂to␈α∞prove
␈↓ ↓H␈↓di␈↓↓␈↓β@␈↓↓␈↓iculties.␈α⊂ It␈α⊂is␈α⊂easy␈α⊂enough␈α⊂to␈α⊂make␈α⊂proof-   ␈↓ εh␈↓theorems␈α
of␈αarithmetic.␈α
 ␈↓↓"If␈α
p␈αis␈α
a␈αprime␈α
number
␈↓ ↓H␈↓checkers␈αfor␈αthe␈αformal␈αsystems␈αin␈αlogic␈αand␈αset  ␈↓ εh␈↓↓and␈α
p␈α
divides␈α
the␈α
product␈α
ab,␈α
then␈α
p␈α
divides␈αa
␈↓ ↓H␈↓theory␈αtextbooks,␈αand␈αwe␈αdid␈αit␈αsome␈αyears␈αago.   ␈↓ εh␈↓↓or␈αp␈αdivides␈αb."␈↓␈αis␈αa␈αtypical␈αsimple␈αexample␈αthat
␈↓ ↓H␈↓The␈α
di␈↓↓␈↓β@␈↓↓␈↓iculty␈αis␈α
that␈α
the␈αformal␈α
proofs␈α
of␈αeasy   ␈↓ εh␈↓is␈αnot␈αjust␈αan␈αinduction␈αon␈αthe␈αstatement␈αof␈αthe
␈↓ ↓H␈↓theorems␈α∞turn␈α∂out␈α∞to␈α∞be␈α∂ten␈α∞times␈α∂longer␈α∞than     ␈↓ εh␈↓problem.
␈↓ ↓H␈↓informal␈αproofs,␈αand␈αthe␈αexcess␈αin␈αlength␈αgrows
␈↓ ↓H␈↓the␈α
further␈α
one␈αadvances␈α
into␈α
the␈α
theory.␈α The   ␈↓ εh␈↓(b)␈α∃The␈α∃adequacy␈α∃of␈α∃FOL's␈α∃set␈α∃theory␈α∃was
␈↓ ↓H␈↓trouble␈α is␈α∨that␈α mathematicians␈α have␈α∨not        ␈↓ εh␈↓tested␈α!by␈α checking␈α!proofs␈α!of␈α Lagrange's
␈↓ ↓H␈↓succeeded␈α&in␈α&completely␈α&formalizing␈α&the       ␈↓ εh␈↓theorem␈αand␈αRamsey's␈αtheorem.␈α These␈αare␈αwell
␈↓ ↓H␈↓languages␈αand␈αreasoning␈αprocesses␈αthey␈αactually␈↓ εh␈↓known␈α∩theorems␈α∩of␈α∪mathematics.␈α∩ [Lagrange's
␈↓ ↓H␈↓use.␈α∂ Much␈α∂reasoning␈α∂that␈α∂at␈α∂␈↓↓␈↓βC␈↓↓␈↓rst␈α∂seems␈α∂to␈α∞be     ␈↓ εh␈↓theorem:␈αthe␈αorder␈αof␈αa␈αsubgroup␈αof␈αa␈αgroup␈αG
␈↓ ↓H␈↓within␈α
a␈α
given␈α
mathematical␈α
system,␈α
actually␈α
is ␈↓ εh␈↓divides␈αthe␈αorder␈αof␈α
G;␈αRamsey's␈αtheorem:␈αlet␈α
G
␈↓ ↓H␈↓metamathematical␈α⊃reasoning␈α⊃about␈α⊃the␈α⊂system.  ␈↓ εh␈↓be␈αa␈αcountably␈α
in␈↓↓␈↓βC␈↓↓␈↓nite␈αset␈αof␈αpoints,␈α
each␈αpoint
␈↓ ↓H␈↓Even␈α
when␈α
a␈αmathematician␈α
is␈α
working␈αwithin     ␈↓ εh␈↓being␈α∪connected␈α∪to␈α∪every␈α∪other␈α∪by␈α∪a␈α∩thread,
␈↓ ↓H␈↓α␈↓ εP␈↓ I5


␈↓ ↓H␈↓each␈α
thread␈α
being␈α
red␈αor␈α
black.␈α
 Then␈α
there␈αis    ␈↓ εh␈↓example␈α⊂below.␈α⊂ Here␈α⊂are␈α⊂three␈α⊂of␈α⊃our␈α⊂recent
␈↓ ↓H␈↓an␈α∞in␈↓↓␈↓βC␈↓↓␈↓nite␈α
subset␈α∞of␈α
these␈α∞points␈α
such␈α∞that␈α
the   ␈↓ εh␈↓experiments:
␈↓ ↓H␈↓connecting␈α∞threads␈α
within␈α∞the␈α
subset␈α∞are␈α∞all␈α
of
␈↓ ↓H␈↓the same color.]                          ␈↓ εh␈↓        Filman␈α∃(Filman,␈α∃in␈α∃progress)␈α∃has␈α∀used
                                          ␈↓ εh␈↓FOL␈α⊃to␈α⊃show␈α⊂that␈α⊃the␈α⊃reasoning␈α⊃involved␈α⊂in
␈↓ ↓H␈↓(c)␈αWilson's␈αtheorem␈αthat␈α"If␈α␈↓↓p␈↓␈αis␈αprime,␈αthen␈α␈↓↓p␈↓   ␈↓ εh␈↓the␈α~solution␈α→of␈α~a␈α→hard␈α~retrospective␈α→chess
␈↓ ↓H␈↓divides␈α␈↓↓(p-1)!␈↓"␈αis␈αa␈αpurely␈α
arithmetic␈αstatement,␈↓ εh␈↓problem␈α∞can␈α∞be␈α∂formalized␈α∞in␈α∞␈↓↓␈↓βC␈↓↓␈↓rst␈α∂order␈α∞logic.
␈↓ ↓H␈↓but␈α!its␈α!proof␈α!uses␈α!a␈α"pairing␈α!argument           ␈↓ εh␈↓We␈α)chose␈α)this␈α)example␈α)from␈α(outside
␈↓ ↓H␈↓(requiring␈α↔set␈α_theory)␈α↔which␈α↔is␈α_beyond␈α↔the      ␈↓ εh␈↓mathematics,␈α∀because␈α∀human␈α∃reasoning␈α∀often
␈↓ ↓H␈↓capability␈α6of␈α6present␈α5theorem-proving        ␈↓ εh␈↓mixes␈α
deduction␈α
with␈α
observation␈α
of␈α
the␈α
outside
␈↓ ↓H␈↓programs.                                 ␈↓ εh␈↓world,␈α→and␈α~observation␈α→of␈α→a␈α~chess␈α→␈↓↓partial
                                          ␈↓ εh␈↓↓position␈↓␈α∀is␈α∃prominent␈α∀in␈α∀this␈α∃example.␈α∀ The
␈↓ ↓H␈↓(d)␈αWe␈αchecked␈α
the␈α␈↓↓␈↓βC␈↓↓␈↓rst␈αone␈α
hundred␈αtheorems     ␈↓ εh␈↓semantic␈α∪attachment␈α∩mechanism␈α∪of␈α∪FOL␈α∩was
␈↓ ↓H␈↓of␈α∃set␈α∃theory␈α∀as␈α∃presented␈α∃in␈α∃(Kelley␈α∀1955).     ␈↓ εh␈↓used␈α∂to␈α∞build␈α∂a␈α∂simulation␈α∞of␈α∂his␈α∂chess␈α∞world.
␈↓ ↓H␈↓This␈α∞established␈α
a␈α∞large␈α
collection␈α∞of␈α∞proofs␈α
to ␈↓ εh␈↓He␈α⊃could␈α⊂then␈α⊃use␈α⊂the␈α⊃semantic␈α⊂simpli␈↓↓␈↓βC␈↓↓␈↓cation
␈↓ ↓H␈↓be␈α∂used␈α∂as␈α∂benchmarks␈α∂to␈α∂measure␈α∂later␈α∞ideas     ␈↓ εh␈↓routines␈α⊃of␈α⊃FOL␈α⊃to␈α⊃answer␈α⊃(in␈α⊃a␈α⊃single␈α⊃step)
␈↓ ↓H␈↓for shortening proofs.                    ␈↓ εh␈↓questions␈α⊃like␈α⊃"is␈α⊃the␈α⊂black␈α⊃king␈α⊃in␈α⊃check␈α⊂on
                                          ␈↓ εh␈↓board␈α∞B"␈α∞by␈α∞looking␈α
at␈α∞the␈α∞model␈α∞rather␈α
than
␈↓ ↓H␈↓(e)␈α∩The␈α∩problem␈α∩of␈α∩formalizing␈α∩how␈α∪we␈α∩can        ␈↓ εh␈↓deducing␈α⊂from␈α∂axioms␈α⊂giving␈α∂the␈α⊂positions␈α∂of
␈↓ ↓H␈↓reason␈α↔about␈α↔what␈α↔other␈α↔people␈α_know␈α↔was         ␈↓ εh␈↓the␈α∂pieces␈α∞and␈α∂others␈α∂about␈α∞the␈α∂rules␈α∂of␈α∞chess
␈↓ ↓H␈↓studied␈α"by␈α#axiomatizing␈α"the␈α#"wise␈α"man          ␈↓ εh␈↓that␈α∩black␈α∩was␈α∩in␈α∩check.␈α∩ This␈α∩single␈α∩use␈α∩of
␈↓ ↓H␈↓problem"␈α∪(McCarthy␈α∪␈↓↓et.␈α∩al␈↓␈α∪1977e)␈α∪and␈α∩(Sato      ␈↓ εh␈↓semantic␈α≠attachment␈α~saves␈α≠several␈α~hundred
␈↓ ↓H␈↓1977).␈α∃ This␈α∃was␈α∃perhaps␈α∃the␈α∃␈↓↓␈↓βC␈↓↓␈↓rst␈α∀extended      ␈↓ εh␈↓steps␈α⊂over␈α⊂traditional␈α⊂formalizations.␈α⊂ Filman's
␈↓ ↓H␈↓application␈αof␈αa␈αformalization␈αof␈αknowledge.␈α It␈↓ εh␈↓proof␈α∩is␈α∩still␈α∪much␈α∩longer␈α∩than␈α∪the␈α∩informal
␈↓ ↓H␈↓took␈αthe␈αfact␈αthat␈αthe␈α␈↓↓␈↓βC␈↓↓␈↓rst␈αand␈αsecond␈αwise␈αmen    ␈↓ εh␈↓proof,␈α showing␈α that␈α∨we␈α still␈α don't␈α∨fully
␈↓ ↓H␈↓didn't␈α⊃know␈α⊃the␈α∩colors␈α⊃of␈α⊃their␈α⊃own␈α∩spots␈α⊃as      ␈↓ εh␈↓understand␈α⊃how␈α⊂humans␈α⊃combine␈α⊂observation
␈↓ ↓H␈↓hypotheses.␈α_ The␈α↔problem␈α_of␈α_proving␈α↔non-       ␈↓ εh␈↓with deduction.
␈↓ ↓H␈↓knowledge␈α⊗by␈α↔assuming␈α⊗that␈α⊗a␈α↔person␈α⊗only
␈↓ ↓H␈↓knows␈α∂what␈α∂follows␈α∂from␈α∞what␈α∂he␈α∂is␈α∂stated␈α∞to      ␈↓ εh␈↓        We␈α∃have␈α⊗preliminary␈α∃estimates␈α⊗of␈α∃the
␈↓ ↓H␈↓know␈αhas␈αnot␈αbeen␈αtreated␈αin␈αthe␈αphilosophical   ␈↓ εh␈↓length␈α"of␈α"the␈α!Kelley␈α"set␈α"theory␈α!proofs
␈↓ ↓H␈↓or␈α≥AI␈α≥literature.␈α≤ Chris␈α≥Goad␈α≥and␈α≤John          ␈↓ εh␈↓mentioned␈α↔above.␈α_ In␈α↔an␈α_initial␈α↔experiment
␈↓ ↓H␈↓McCarthy␈α!(separately)␈α!have␈α!attacked␈α!this      ␈↓ εh␈↓using␈α→only␈α→part␈α→of␈α→the␈α~currently␈α→available
␈↓ ↓H␈↓problem,␈α∃which␈α∃has␈α∀turned␈α∃out␈α∃to␈α∃be␈α∀quite        ␈↓ εh␈↓features,␈α~we␈α~reduced␈α~the␈α~number␈α~of␈α→steps
␈↓ ↓H␈↓di␈↓↓␈↓β@␈↓↓␈↓icult and deep.                        ␈↓ εh␈↓necessary␈α"to␈α"prove␈α"the␈α#␈↓↓␈↓βC␈↓↓␈↓rst␈α"thirty-three
                                          ␈↓ εh␈↓theorems␈α
from␈α
461␈α
to␈α
104.␈α
 Considering␈α
that␈α
it
␈↓ ↓H␈↓(f)␈α
We␈α
proved␈αthe␈α
correctness␈α
of␈αthe␈α
McCarthy-   ␈↓ εh␈↓takes␈α
one␈α
step␈α
just␈αto␈α
express␈α
the␈α
theorem,␈αthis
␈↓ ↓H␈↓Painter␈αcompiler␈α(McCarthy␈αand␈αPainter␈α1967).  ␈↓ εh␈↓is␈αquite␈αimpressive.␈α We␈αexpect␈αthat␈αadding␈αthe
␈↓ ↓H␈↓This␈α⊃allowed␈α⊃us␈α⊃to␈α⊃compare␈α⊃the␈α⊃original␈α⊃␈↓↓␈↓βC␈↓↓␈↓rst     ␈↓ εh␈↓goal-structure␈α↔features␈α⊗mentioned␈α↔below␈α⊗will
␈↓ ↓H␈↓order␈α_proof␈α_with␈α_some␈α_more␈α_recent␈α_proofs        ␈↓ εh␈↓substantially reduce these proof lengths.
␈↓ ↓H␈↓(Weyhrauch␈α≠and␈α≤Milner␈α≠1972;␈α≤Boyer␈α≠and
␈↓ ↓H␈↓Moore 1975).                              ␈↓ εh␈↓        In␈α→connection␈α→with␈α→McCarthy's␈α_recent
                                          ␈↓ εh␈↓(McCarthy␈α!1977d)␈α!formalization␈α!of␈α!LISP
␈↓ ↓H␈↓        After␈αa␈αperiod␈αof␈αadding␈αnew␈α
features␈αto ␈↓ εh␈↓programs␈α
using␈α
sentences␈α
and␈α
schemata␈α∞of␈α
␈↓↓␈↓βC␈↓↓␈↓rst
␈↓ ↓H␈↓FOL␈α
we␈αhave␈α
again␈αbegun␈α
to␈α
experiment␈αwith       ␈↓ εh␈↓order␈α∂logic,␈α∞we␈α∂have␈α∂checked␈α∞a␈α∂FOL␈α∂proof␈α∞of
␈↓ ↓H␈↓proofs␈α
and␈α
our␈α
initial␈α
successes␈α
are␈α
encouraging.␈↓ εh␈↓the␈α~correctness␈α→of␈α~his␈α~␈↓↓samefringe␈↓␈α→program.
␈↓ ↓H␈↓These␈α⊃recent␈α⊃improvements␈α⊃have␈α⊃reduced␈α⊃the     ␈↓ εh␈↓(␈↓↓samefringe[x,y]␈↓␈α∂is␈α∂true␈α∞if␈α∂the␈α∂S-expressions␈α∞␈↓↓x␈↓
␈↓ ↓H␈↓length␈αof␈αsome␈α
proofs␈αby␈αa␈α
factor␈αof␈αbetter␈α
than   ␈↓ εh␈↓and␈α␈↓↓y␈↓␈αhave␈αthe␈αsame␈αatoms␈αin␈αthe␈α
same␈αorder).
␈↓ ↓H␈↓ten.␈α Some␈αof␈αthe␈αproofs␈αwe␈αare␈αnow␈αproducing     ␈↓ εh␈↓The␈αproof␈αas␈αchecked␈αby␈αFOL␈αwas␈αof␈αthe␈αsame
␈↓ ↓H␈↓are␈α⊃about␈α⊃as␈α∩long␈α⊃as␈α⊃their␈α∩informal␈α⊃versions.    ␈↓ εh␈↓length␈α⊂as␈α∂a␈α⊂written␈α⊂out␈α∂informal␈α⊂proof␈α⊂of␈α∂the
␈↓ ↓H␈↓This␈α∂is␈α∞most␈α∂clearly␈α∞evident␈α∂in␈α∂the␈α∞␈↓↓samefringe␈↓   ␈↓ εh␈↓same␈α∩result.␈α∩ We␈α∩believe␈α∩that␈α∪such␈α∩favorable
                                          ␈↓ εh␈↓results are generally possible.
␈↓ ↓H␈↓α␈↓ εP␈↓ J6


␈↓ ↓H␈↓        Our plans for FOL include the following:␈↓ εh␈↓correctness␈α∀are␈α∃often␈α∀simpler␈α∀than␈α∃proofs␈α∀of
                                          ␈↓ εh␈↓program␈α?␈αεcorrectness,␈α?␈απbecause␈α?␈αεoften
␈↓ ↓H␈↓(1)␈α∞The␈α∞veri␈↓↓␈↓βC␈↓↓␈↓cation␈α∞of␈α∞the␈α∞correctness␈α∞of␈α
LISP   ␈↓ εh␈↓mathematical induction is not required.
␈↓ ↓H␈↓programs.␈α⊂ John␈α⊂McCarthy␈α⊃(McCarthy␈α⊂1977d)
␈↓ ↓H␈↓has␈α∃recently␈α∃begun␈α∃using␈α∃axiom␈α∃schemas␈α∃to       ␈↓ εh␈↓(4)␈α∂We␈α∂intend␈α⊂to␈α∂redo␈α∂the␈α∂theorems␈α⊂of␈α∂Kelley
␈↓ ↓H␈↓prove␈α∩the␈α∩properties␈α∩of␈α∩LISP␈α∩programs.␈α⊃ We      ␈↓ εh␈↓mentioned␈α∞above␈α∞using␈α
the␈α∞many␈α∞new␈α
features
␈↓ ↓H␈↓intend␈α⊗to␈α⊗expand␈α⊗this␈α⊗work␈α⊗by␈α∃introducing       ␈↓ εh␈↓that␈α∞have␈α∞been␈α
added␈α∞to␈α∞FOL.␈α∞ These␈α
include
␈↓ ↓H␈↓meta-mathematical␈α∃machinery␈α∃into␈α∃FOL␈α∃(see     ␈↓ εh␈↓the␈αsyntactic␈αsimpli␈↓↓␈↓βC␈↓↓␈↓er,␈αthe␈α
semantic␈αattachment
␈↓ ↓H␈↓below).␈α This␈αwill␈αbe␈αfollowed␈αby␈αa␈αmajor␈αe␈↓↓␈↓β@␈↓↓␈↓ort   ␈↓ εh␈↓mechanism, and various decision procedures.
␈↓ ↓H␈↓to␈α
use␈α
McCarthy's␈α
axiomatization␈α
of␈α
LISP␈αand
␈↓ ↓H␈↓to␈α⊂prove␈α⊂properties␈α⊂of␈α⊂simple␈α⊂LISP␈α∂programs.    ␈↓ εh␈↓(5)␈α→Introducing␈α→metamathematical␈α_machinery
␈↓ ↓H␈↓Weyhrauch␈α⊂has␈α⊂recently␈α⊂pointed␈α⊂out␈α⊂that␈α⊂this    ␈↓ εh␈↓into␈α∃FOL␈α∀will␈α∃allow␈α∃us␈α∀to␈α∃state␈α∃and␈α∀prove
␈↓ ↓H␈↓same␈α∂technique␈α∂can␈α∞be␈α∂used␈α∂to␈α∂formulate␈α∞part     ␈↓ εh␈↓theorems␈α∩about␈α∩how␈α∩we␈α∩do␈α∩reasoning␈α∩in␈α∩the
␈↓ ↓H␈↓of␈αDana␈αScott's␈αcomputation␈αinduction␈αinto␈α␈↓↓␈↓βC␈↓↓␈↓rst ␈↓ εh␈↓logic.␈α In␈α
particular,␈αwe␈αwill␈α
be␈αable␈αto␈α
establish,
␈↓ ↓H␈↓order␈α-logic.␈α- This␈α-also␈α.requires␈α-the           ␈↓ εh␈↓as␈α≤sentences␈α≤of␈α≤the␈α≤metamathematics,␈α≠new
␈↓ ↓H␈↓metamathematical␈α∩machinery.␈α⊃ We␈α∩expect␈α⊃this   ␈↓ εh␈↓axiom␈α∀schemas␈α∀that␈α∀can␈α∀be␈α∀used␈α∀in␈α∪further
␈↓ ↓H␈↓to␈α∩be␈α∩su␈↓↓␈↓β@␈↓↓␈↓iciently␈α∪practical␈α∩for␈α∩us␈α∩to␈α∪use␈α∩this    ␈↓ εh␈↓proofs.␈α≤ This␈α≤will␈α≤be␈α≤especially␈α≤useful␈α≠in
␈↓ ↓H␈↓axiomatization in Stanford LISP courses.  ␈↓ εh␈↓proving␈α∂the␈α∂correctness␈α∂of␈α⊂recursive␈α∂programs.
                                          ␈↓ εh␈↓Another␈α(application␈α(of␈α(schemas␈α(is␈α'to
␈↓ ↓H␈↓(2)␈α∩Another␈α∩aspect␈α∩of␈α∩program␈α∩veri␈↓↓␈↓βC␈↓↓␈↓cation␈α⊃is    ␈↓ εh␈↓axiomatizing circumscription.
␈↓ ↓H␈↓what␈α∨are␈α∨called␈α∨intensional␈α∨properties␈α≡of
␈↓ ↓H␈↓programs.␈α These␈αinclude␈αthings␈αlike␈αhow␈αmuch   ␈↓ εh␈↓(6)␈α
The␈α
usefulness␈αof␈α
the␈α
metamathematics␈αwill
␈↓ ↓H␈↓storage␈αa␈α
program␈αuses,␈αand␈α
how␈αmany␈α
steps␈αit     ␈↓ εh␈↓be␈α⊗enhanced␈α∃by␈α⊗certain␈α⊗re␈↓↓␈↓βD␈↓↓␈↓ection␈α∃principles.
␈↓ ↓H␈↓takes.␈α⊗ These␈α∃questions␈α⊗cannot␈α∃be␈α⊗asked␈α∃by      ␈↓ εh␈↓These␈α
are␈αrules␈α
that␈αstate␈α
some␈αrelation␈α
between
␈↓ ↓H␈↓current␈α∂formalisms␈α∂for␈α∂mathematical␈α⊂theory␈α∂of  ␈↓ εh␈↓a␈α"theory␈α"and␈α"its␈α"metamathematics.␈α! For
␈↓ ↓H␈↓computation.␈α" They␈α"require␈α#theories␈α"that      ␈↓ εh␈↓example,␈αif␈αyou␈αhave␈αproved␈αa␈αcertain␈αformula,
␈↓ ↓H␈↓contain␈αprograms␈αas␈αobjects␈αand␈αcan␈αtalk␈αabout   ␈↓ εh␈↓then␈αin␈αthe␈αmeta-theory␈αyou␈αcan␈αassert␈αthat␈αthe
␈↓ ↓H␈↓the␈α∀abstract␈α∀properties␈α∀of␈α∀the␈α∀machines␈α∀that    ␈↓ εh␈↓formula␈α≤is␈α≤provable.␈α≥ Conversely,␈α≤informal
␈↓ ↓H␈↓they␈αrun␈αon.␈α
 Most␈αprevious␈αformal␈αe␈↓↓␈↓β@␈↓↓␈↓orts␈α
have   ␈↓ εh␈↓mathematics␈α'often␈α'uses␈α&metamathematical
␈↓ ↓H␈↓only␈α shown␈α∨properties␈α of␈α the␈α∨algorithms        ␈↓ εh␈↓assertions␈α that␈α!all␈α formulas␈α!with␈α certain
␈↓ ↓H␈↓computed␈α≥by␈α≡programs,␈α≥not␈α≡properties␈α≥of        ␈↓ εh␈↓properties␈α
are␈α
true.␈α
 The␈αattachment␈α
mechanism
␈↓ ↓H␈↓programs␈α⊃themselves.␈α⊃ One␈α⊃exception␈α⊃was␈α⊃the    ␈↓ εh␈↓combined␈α
with␈αre␈↓↓␈↓βD␈↓↓␈↓ection␈α
principles␈α
will␈αallow␈α
us
␈↓ ↓H␈↓work␈α∞of␈α∞Aiello,␈α∞Aiello,␈α∞and␈α∞Weyhrauch␈α
(Aiello   ␈↓ εh␈↓to␈α~automatically␈α~use␈α~such␈α≠metatheorems␈α~to
␈↓ ↓H␈↓1974)␈α
on␈α
PASCAL.␈α This␈α
was␈α
carried␈αout␈α
using     ␈↓ εh␈↓prove theorems in the base theory.
␈↓ ↓H␈↓another␈αformal␈αsystem␈αand␈αwe␈αhave␈α
just␈αbegun
␈↓ ↓H␈↓to␈α∞think␈α∞about␈α∞such␈α∞problems␈α∞using␈α∞␈↓↓␈↓βC␈↓↓␈↓rst␈α∞order    ␈↓ εh␈↓α␈↓ πuOrganization of the work 
␈↓ ↓H␈↓logic.␈α⊃ One␈α⊂approach␈α⊃is␈α⊂to␈α⊃take␈α⊃advantage␈α⊂of
␈↓ ↓H␈↓the␈α→fact␈α_that␈α→intensional␈α_properties␈α→of␈α_one     ␈↓ εh␈↓        The␈α∞work␈α∞is␈α∞under␈α∞the␈α∞general␈α∞direction
␈↓ ↓H␈↓program␈α∩are␈α∩extensional␈α∩properties␈α∩of␈α⊃certain  ␈↓ εh␈↓of␈α&John␈α%McCarthy␈α&who␈α&also␈α%develops
␈↓ ↓H␈↓related programs.                         ␈↓ εh␈↓formalizations␈α↔and␈α_general␈α↔theory␈α_and␈α↔uses
                                          ␈↓ εh␈↓FOL␈α_to␈α_check␈α_out␈α_formalizations.␈α_ Richard
␈↓ ↓H␈↓(3)␈α≤The␈α≠veri␈↓↓␈↓βC␈↓↓␈↓cation␈α≤of␈α≠the␈α≤correctness␈α≠of       ␈↓ εh␈↓Weyhrauch␈α→is␈α→the␈α→main␈α→developer␈α→of␈α_and
␈↓ ↓H␈↓hardware␈α∞circuit␈α∞design␈α∞using␈α∞FOL␈α
continuing   ␈↓ εh␈↓implementer␈α_of␈α_FOL␈α↔and␈α_is␈α_also␈α↔pursuing
␈↓ ↓H␈↓the␈α
work␈α
of␈αWagner␈α
(Wagner␈α
1977).␈α Almost␈α
all    ␈↓ εh␈↓research␈α≤making␈α≤metamathematical␈α≠methods
␈↓ ↓H␈↓present␈α≤hardware␈α≤veri␈↓↓␈↓βC␈↓↓␈↓cation␈α≤is␈α≥based␈α≤on       ␈↓ εh␈↓available␈α∩in␈α∩it.␈α∩ Graduate␈α∩students␈α∩help␈α∩with
␈↓ ↓H␈↓simulating␈α∃it␈α∃in␈α∃all␈α∃possible␈α⊗states.␈α∃ Wagner   ␈↓ εh␈↓implementations␈α∂and␈α∂pursue␈α∂thesis␈α∂research␈α∂in
␈↓ ↓H␈↓demonstrated␈α≥that␈α≥formal␈α≥proofs␈α≥that␈α≤the       ␈↓ εh␈↓arti␈↓↓␈↓βC␈↓↓␈↓cial␈α7intelligence␈α7(concentrating␈α6on
␈↓ ↓H␈↓hardware␈αis␈α
correct␈αare␈α
feasible␈αand␈αrequire␈α
less␈↓ εh␈↓epistemological␈α∂problems)␈α∂and␈α∂in␈α∞mathematical
␈↓ ↓H␈↓human␈αand␈αcomputer␈αwork␈αthan␈αthe␈αsimulation     ␈↓ εh␈↓theory␈α~of␈α≠computation.␈α~ The␈α≠group␈α~shares
␈↓ ↓H␈↓techniques.␈α! In␈α"fact␈α!proofs␈α"of␈α!hardware        ␈↓ εh␈↓interests␈α⊂with␈α⊂the␈α⊂separately␈α⊃supported␈α⊂groups
␈↓ ↓H␈↓α␈↓ εP␈↓ J7


␈↓ ↓H␈↓in␈α⊗mathematical␈α↔theory␈α⊗of␈α↔computation␈α⊗and      ␈↓ εh␈↓A.M. Turing Award from Association for
␈↓ ↓H␈↓theorem␈α⊃proving.␈α⊃ Both␈α⊃the␈α∩epistemology␈α⊃and    ␈↓ εh␈↓␈↓ π(Computing Machinery (1971).
␈↓ ↓H␈↓the␈α∂proof-checking␈α∞have␈α∂excited␈α∂much␈α∞outside
␈↓ ↓H␈↓interest,␈α∀and␈α∀we␈α∀propose␈α∀a␈α∀rotating␈α∀research    ␈↓ εh␈↓PROFESSIONAL EXPERIENCE:
␈↓ ↓H␈↓associateship␈α→for␈α→recent␈α→PhDs␈α→interested␈α_in    ␈↓ εh␈↓Proctor Fellow, Princeton University (1950-51),
␈↓ ↓H␈↓contributing to the work and learning from it.␈↓ εh␈↓Higgins Research Instructor in Mathematics,
                                          ␈↓ εh␈↓␈↓ π(Princeton University (1951-53),
␈↓ ↓H␈↓α␈↓ βCFacilities                                ␈↓ εh␈↓Acting Assistant Professor of Mathematics,
                                          ␈↓ εh␈↓␈↓ π(Stanford University (1953-55),
␈↓ ↓H␈↓        The␈α
project␈α
will␈α∞be␈α
part␈α
of␈α∞the␈α
Stanford ␈↓ εh␈↓Assistant Professor of Mathematics, Dartmouth
␈↓ ↓H␈↓University␈α≥Arti␈↓↓␈↓βC␈↓↓␈↓cial␈α≥Intelligence␈α≥Laboratory ␈↓ εh␈↓␈↓ π(College (1955-58),
␈↓ ↓H␈↓and␈α~will␈α~use␈α~its␈α~computer␈α≠facilities.␈α~ This     ␈↓ εh␈↓Assistant Professor of Communication Science,
␈↓ ↓H␈↓Laboratory␈α∞is␈α∞directed␈α
by␈α∞John␈α∞McCarthy␈α
and     ␈↓ εh␈↓␈↓ π(M.I.T. (1958-61),
␈↓ ↓H␈↓has␈α⊃been␈α⊃mainly␈α⊃supported␈α⊃by␈α⊃ARPA␈α⊃in␈α⊂the         ␈↓ εh␈↓Associate Professor of Communication Science,
␈↓ ↓H␈↓past,␈α
but␈α
the␈αfraction␈α
of␈α
its␈α
support␈αprovided␈α
by ␈↓ εh␈↓␈↓ π(M.I.T. (1961-62),
␈↓ ↓H␈↓ARPA is diminishing.                      ␈↓ εh␈↓Professor of Computer Science Stanford
                                          ␈↓ εh␈↓␈↓ π(University (1962 - present).
␈↓ ↓H␈↓The␈α⊃Laboratory␈α⊃computer␈α⊃facility␈α⊃is␈α⊃generally
␈↓ ↓H␈↓adequate␈α
for␈αthis␈α
work␈α
and␈αthere␈α
are␈α
no␈αdirect    ␈↓ εh␈↓PROFESSIONAL RESPONSIBILITIES
␈↓ ↓H␈↓charges␈α∃for␈α∃computer␈α∃time␈α∃in␈α⊗this␈α∃proposal.     ␈↓ εh␈↓␈↓ π(AND SCIENTIFIC INTERESTS:
␈↓ ↓H␈↓However,␈αthere␈αare␈αbudget␈αitems␈αfor␈αa␈αshare␈αof    ␈↓ εh␈↓With Marvin Minsky organized and directed
␈↓ ↓H␈↓a␈α~computer␈α→technician␈α~and␈α~some␈α→computer        ␈↓ εh␈↓␈↓ π(the Arti␈↓↓␈↓βC␈↓↓␈↓cial Intelligence Project at M.I.T.
␈↓ ↓H␈↓maintenance␈α⊂costs.␈α⊂ In␈α⊂addition,␈α⊂there␈α⊃are␈α⊂two  ␈↓ εh␈↓Organized and directs Stanford Arti␈↓↓␈↓βC␈↓↓␈↓cial
␈↓ ↓H␈↓computer␈α∞terminals␈α∞budgeted␈α∞at␈α∞$2,500␈α∞each␈α
to   ␈↓ εh␈↓␈↓ π(Intelligence Project.
␈↓ ↓H␈↓provide␈α∂remote␈α∂access␈α∞to␈α∂the␈α∂computer␈α∂for␈α∞the    ␈↓ εh␈↓Developed the LISP programming system for
␈↓ ↓H␈↓participants␈α⊂in␈α⊂this␈α⊂project.␈α⊂ The␈α⊂total␈α⊂cost␈α∂of ␈↓ εh␈↓␈↓ π(computing with symbolic expressions,
␈↓ ↓H␈↓computer␈α↔facilities␈α↔provided␈α↔in␈α↔this␈α_way␈α↔is     ␈↓ εh␈↓␈↓ π(participated in the development of the
␈↓ ↓H␈↓substantially␈α
less␈αthan␈α
it␈α
would␈αbe␈α
on␈α
the␈αbasis  ␈↓ εh␈↓␈↓ π(ALGOL 58 and the ALGOL 60
␈↓ ↓H␈↓of direct charges for computer time used. ␈↓ εh␈↓␈↓ π(languages.
                                          ␈↓ εh␈↓Present scienti␈↓↓␈↓βC␈↓↓␈↓c work is in the ␈↓↓␈↓βC␈↓↓␈↓elds of
␈↓ ↓H␈↓α␈↓ β?Personnel                                 ␈↓ εh␈↓␈↓ π(Arti␈↓↓␈↓βC␈↓↓␈↓cial Intelligence, Computation with
                                          ␈↓ εh␈↓␈↓ π(Symbolic Expressions, Mathematical
␈↓ ↓H␈↓α␈↓ α9Biography of John McCarthy                ␈↓ εh␈↓␈↓ π(Theory of Computation, Time-Sharing
                                          ␈↓ εh␈↓␈↓ π(computer systems.
␈↓ ↓H␈↓BORN:  September 4, 1927 in Boston,       ␈↓ εh␈↓PUBLICATIONS:
␈↓ ↓H␈↓␈↓ αλMassachusetts                             ␈↓ εh␈↓[1]  "Towards a Mathematical Theory of
                                          ␈↓ εh␈↓␈↓ π(Computation", in ␈↓↓Proc. IFIP Congress 62␈↓,
␈↓ ↓H␈↓EDUCATION:                                ␈↓ εh␈↓␈↓ π(North-Holland, Amsterdam, 1963.
␈↓ ↓H␈↓B.S.  (Mathematics) California Institute of␈↓ εh␈↓[2]  "A Basis for a Mathematical Theory of
␈↓ ↓H␈↓␈↓ αλTechnology, 1948.                         ␈↓ εh␈↓␈↓ π(Computation", in P. Bra␈↓↓␈↓β@␈↓↓␈↓ort and D.
␈↓ ↓H␈↓Ph.D. (Mathematics) Princeton University, ␈↓ εh␈↓␈↓ π(Hershberg (eds.), ␈↓↓Computer Programming
␈↓ ↓H␈↓␈↓ αλ1951.                                     ␈↓ εh␈↓↓␈↓ π(and Formal Systems␈↓, North-Holland,
                                          ␈↓ εh␈↓␈↓ π(Amsterdam, 1963.
␈↓ ↓H␈↓HONORS AND SOCIETIES:                     ␈↓ εh␈↓[3]  (with S. Boilen, E. Fredkin, J.C.R.
␈↓ ↓H␈↓American Mathematical Society,            ␈↓ εh␈↓␈↓ π(Licklider) "A Time-Sharing Debugging
␈↓ ↓H␈↓Association for Computing Machinery,      ␈↓ εh␈↓␈↓ π(System for a Small Computer", ␈↓↓Proc.
␈↓ ↓H␈↓Sigma Xi,                                 ␈↓ εh␈↓↓␈↓ π(AFIPS Conf.␈↓ (SJCC), Vol. 23, 1963.
␈↓ ↓H␈↓Sloan Fellow in Physical Science (1957-59),␈↓ εh␈↓[4]  (with F. Corbato, M. Daggett) "The
␈↓ ↓H␈↓ACM National Lecturer (1961),             ␈↓ εh␈↓␈↓ π(Linking Segment Subprogram Language
␈↓ ↓H␈↓IEEE,                                     ␈↓ εh␈↓␈↓ π(and Linking Loader Programming
                                          ␈↓ εh␈↓␈↓ π(Languages", ␈↓↓Comm. ACM␈↓, July 1963.
␈↓ ↓H␈↓α␈↓ εP␈↓ I8


␈↓ ↓H␈↓[5]  "Problems in the Theory of Computation",␈↓ εh␈↓↓␈↓ π(1975␈↓, The World Book Science Annual,
␈↓ ↓H␈↓␈↓ αλ␈↓↓Proc. IFIP Congress 1965␈↓.                 ␈↓ εh␈↓␈↓ π(Field Enterprises Educational Corporation,
␈↓ ↓H␈↓[6]  "Time-Sharing Computer Systems", in W.␈↓ εh␈↓␈↓ π(Chicago, 1974.
␈↓ ↓H␈↓␈↓ αλOrr (ed.), ␈↓↓Conversational Computers␈↓, Wiley,␈↓ εh␈↓[19]  "The Home Information Terminal,"
␈↓ ↓H␈↓␈↓ αλ1966.                                     ␈↓ εh␈↓␈↓ π(invited presentation, AAAS Annual
␈↓ ↓H␈↓[7]  "A Formal Description of a Subset of ␈↓ εh␈↓␈↓ π(Meeting, Feb. 18-24, 1976, Boston.
␈↓ ↓H␈↓␈↓ αλAlgol", in T.  Steele (ed.), ␈↓↓Formal       ␈↓ εh␈↓[20]  "An Unreasonable Book," a review of
␈↓ ↓H␈↓↓␈↓ αλLanguage Description Languages for        ␈↓ εh␈↓␈↓ π(␈↓↓Computer Power and Human Reason␈↓, by
␈↓ ↓H␈↓↓␈↓ αλComputer Programming␈↓, North-Holland,      ␈↓ εh␈↓␈↓ π(Joseph Weizenbaum (W.H. Freeman and
␈↓ ↓H␈↓␈↓ αλAmsterdam, 1966.                          ␈↓ εh␈↓␈↓ π(Co., San Francisco, 1976) in SIGART
␈↓ ↓H␈↓[8]  "Information", ␈↓↓Scienti␈↓␈↓βS␈↓␈↓↓c American␈↓,   ␈↓ εh␈↓␈↓ π(Newsletter
␈↓ ↓H␈↓␈↓ αλSeptember 1966.                           ␈↓ εh␈↓558, June 1976, also in ␈↓↓Creative Computing␈↓,
␈↓ ↓H␈↓[9]  "Computer Control of a Hand and Eye", in␈↓ εh␈↓␈↓ π(Chestnut Hill, Massachusetts, 1976 and in
␈↓ ↓H␈↓␈↓ αλ␈↓↓Proc.  Third All-Union Conference on      ␈↓ εh␈↓␈↓ π("Three Reviews of J. Weizenbaum's
␈↓ ↓H␈↓↓␈↓ αλAutomatic Control (Technical Cybernetics)␈↓,␈↓ εh␈↓␈↓ π(␈↓↓Computer Power and Human Reason␈↓, (with
␈↓ ↓H␈↓␈↓ αλNauka, Moscow, 1967 (Russian).            ␈↓ εh␈↓␈↓ π(B. Buchanan and J. Lederberg), Stanford
␈↓ ↓H␈↓[10]  (with D. Brian, G. Feldman, and J. Allen)␈↓ εh␈↓␈↓ π(Arti␈↓↓␈↓βC␈↓↓␈↓cial Intelligence Laboratory Memo
␈↓ ↓H␈↓␈↓ αλ"THOR ␈↓↓␈↓βE␈↓↓␈↓ A Display Based Time-             ␈↓ εh␈↓␈↓ π(291, Computer Science Department,
␈↓ ↓H␈↓␈↓ αλSharing System", ␈↓↓Proc. AFIPS Conf.␈↓        ␈↓ εh␈↓␈↓ π(Stanford, November 1976.
␈↓ ↓H␈↓␈↓ αλ(FJCC), Vol.  30, Thompson, Washington,   ␈↓ εh␈↓[21]  Review: ␈↓↓Computer Power and Human
␈↓ ↓H␈↓␈↓ αλD.C., 1967.                               ␈↓ εh␈↓↓␈↓ π(Reason␈↓, by Joseph Weizenbaum (W.H.
␈↓ ↓H␈↓[11]  (with James Painter) "Correctness of a␈↓ εh␈↓␈↓ π(Freeman and Co., San Francisco, 1976) in
␈↓ ↓H␈↓␈↓ αλCompiler for Arithmetic Expressions",     ␈↓ εh␈↓␈↓ π(Physics Today, 1977.
␈↓ ↓H␈↓␈↓ αλAmer. Math. Soc., ␈↓↓Proc. Symposia in       ␈↓ εh␈↓[22]  "The Home Information Terminal" to
␈↓ ↓H␈↓↓␈↓ αλApplied Math., Math. Aspects of           ␈↓ εh␈↓␈↓ π(appear in The Grolier Encyclopedia, 1977,
␈↓ ↓H␈↓↓␈↓ αλComputer Science␈↓, New York, 1967.         ␈↓ εh␈↓␈↓ π(also to appear in ␈↓↓The International
␈↓ ↓H␈↓[12]  "Programs with Common Sense", in    ␈↓ εh␈↓↓␈↓ π(YearBook and Statemen's Who's Who␈↓,
␈↓ ↓H␈↓␈↓ αλMarvin Minsky (ed.), ␈↓↓Semantic Information ␈↓ εh␈↓␈↓ π(Surrey, England, 1977.
␈↓ ↓H␈↓↓␈↓ αλProcessing␈↓, MIT Press, Cambridge, 1968.   ␈↓ εh␈↓[23]  "Dialnet and Home Computers" (with Les
␈↓ ↓H␈↓[13]  (with Lester Earnest, D. Raj. Reddy,␈↓ εh␈↓␈↓ π(Earnest), ␈↓↓Proceedings of the First West
␈↓ ↓H␈↓␈↓ αλPierre Vicens) "A Computer with Hands,    ␈↓ εh␈↓↓␈↓ π(Coast Computer Faire and Conference␈↓, San
␈↓ ↓H␈↓␈↓ αλEyes, and Ears", ␈↓↓Proc. AFIPS Conf.␈↓        ␈↓ εh␈↓␈↓ π(Francisco, April 1977.
␈↓ ↓H␈↓␈↓ αλ(FJCC), 1968.                             ␈↓ εh␈↓[24]  "On The Model Theory of Knowledge"
␈↓ ↓H␈↓[14]  (with Patrick Hayes) "Some Philosophical␈↓ εh␈↓␈↓ π((with M. Sato, S. Igarashi, and T.
␈↓ ↓H␈↓␈↓ αλProblems from the Standpoint of Arti␈↓↓␈↓βC␈↓↓␈↓cial ␈↓ εh␈↓␈↓ π(Hayashi), ␈↓↓Proceedings of the Fifth
␈↓ ↓H␈↓␈↓ αλIntelligence", in Donald Michie (ed.),    ␈↓ εh␈↓↓␈↓ π(International Joint Conference on Arti␈↓␈↓βS␈↓␈↓↓cial
␈↓ ↓H␈↓␈↓ αλ␈↓↓Machine Intelligence 4␈↓, American Elsevier,␈↓ εh␈↓↓␈↓ π(Intelligence␈↓, M.I.T, Cambridge, 1977.
␈↓ ↓H␈↓␈↓ αλNew York, 1969.                           ␈↓ εh␈↓[25]  "Another SAMEFRINGE", in SIGART
␈↓ ↓H␈↓[15]  "The Home Information Terminal", ␈↓↓Man␈↓ εh␈↓␈↓ π(Newsletter No. 61, February 1977.
␈↓ ↓H␈↓↓␈↓ αλand Computer, Proc. Int. Conf.,           ␈↓ εh␈↓[26]  "Ascribing Mental Qualities to Machines"
␈↓ ↓H␈↓↓␈↓ αλBordeaux, 1970␈↓, S. Karger, New York,      ␈↓ εh␈↓␈↓ π(to appear in ␈↓↓Essays in Philosophy and
␈↓ ↓H␈↓␈↓ αλ1972.                                     ␈↓ εh␈↓↓␈↓ π(Computer Technology␈↓, National Symposium
␈↓ ↓H␈↓[16]  "Mechanical Servants for Mankind," in␈↓ εh␈↓␈↓ π(for Philosophy and Computer Technology,
␈↓ ↓H␈↓␈↓ αλ␈↓↓Britannica Yearbook of Science and the    ␈↓ εh␈↓␈↓ π(New York, 1977.
␈↓ ↓H␈↓↓␈↓ αλFuture␈↓, 1973.                             ␈↓ εh␈↓[27]  "Epistemological Problems of Arti␈↓↓␈↓βC␈↓↓␈↓cial
␈↓ ↓H␈↓[17]  Book Review: "Arti␈↓↓␈↓βC␈↓↓␈↓cial Intelligence: A␈↓ εh␈↓␈↓ π(Intelligence", ␈↓↓Proceedings of the Fifth
␈↓ ↓H␈↓␈↓ αλGeneral Survey" by Sir James Lighthill, in␈↓ εh␈↓↓␈↓ π(International Joint Conference on Arti␈↓␈↓βS␈↓␈↓↓cial
␈↓ ↓H␈↓␈↓ αλ␈↓↓Arti␈↓␈↓βS␈↓␈↓↓cial Intelligence, Vol. 5, No. 3␈↓, Fall␈↓ εh␈↓↓␈↓ π(Intelligence␈↓, M.I.T., Cambridge, 1977.
␈↓ ↓H␈↓␈↓ αλ1974.
␈↓ ↓H␈↓[18]  "Modeling Our Minds" in ␈↓↓Science Year
␈↓ ↓H␈↓α␈↓ εP␈↓ J9


␈↓ ↓H␈↓α␈↓ ε!Budget 

␈↓ ↓H␈↓∧PERIOD COVERED: 3 Years: 1 June 1978 through 31 December 1981.

␈↓ ↓H␈↓∧Dates:                     6/1/78-5/31/79   6/1/79-5/31/80   6/1/80-5/31/81

␈↓ ↓H␈↓∧                                   Person-           Person-          Person-
␈↓ ↓H␈↓∧A. SALARIES AND WAGES              months            months           months

␈↓ ↓H␈↓∧   1. Senior Personnel:

␈↓ ↓H␈↓∧     a. John McCarthy,    24,257.    6.5    27,007.    6.5   29,168.    6.5
␈↓ ↓H␈↓∧       Professor
␈↓ ↓H␈↓∧       Summer 75%(2 mos.)
␈↓ ↓H␈↓∧       Acad. Yr. 50%

␈↓ ↓H␈↓∧   2. Other Personnel


␈↓ ↓H␈↓∧     a. Student Research 
␈↓ ↓H␈↓∧        Assistants
␈↓ ↓H␈↓∧        (50% Acad.Yr.;
␈↓ ↓H␈↓∧        100% Summer)

␈↓ ↓H␈↓∧       (1)Carolyn Talcott  7,155.    7.5     7,704.    7.5    8,320.    7.5

␈↓ ↓H␈↓∧       (2)                 7,155.    7.5     7,704.    7.5    8,320.    7.5

␈↓ ↓H␈↓∧     b. Support Personnel

␈↓ ↓H␈↓∧       (1) Sec'y (20%)     2,092.    2.4     2,259.    2.4    2,440.    2.4

␈↓ ↓H␈↓∧       (2) Sys.Prog.(15%)  2,937.    1.8     3,172.    1.8    3,426.    1.8
␈↓ ↓H␈↓∧                          _______           _______          _______

␈↓ ↓H␈↓∧   Total Salaries & Wages 43,596.           47,846.          51,674.

␈↓ ↓H␈↓∧B. STAFF BENEFITS         
␈↓ ↓H␈↓∧   9/1/77-8/31/78:19.0%          
␈↓ ↓H␈↓∧   9/1/78-8/31/79:20.3%
␈↓ ↓H␈↓∧   9/1/79-8/31/80;21.6%                                          
␈↓ ↓H␈↓∧   9/1/80-8/31/81;22.4%
␈↓ ↓H␈↓∧                           8,708.           10,179.          11,472.
␈↓ ↓H␈↓∧                          _______          ________         ________
␈↓ ↓H␈↓∧C. TOTAL SALARIES, WAGES,
␈↓ ↓H␈↓∧   AND STAFF BENEFITS     52,304.           58,025.          63,146.
␈↓ ↓H␈↓α␈↓ εP␈↓ :10


␈↓ ↓H␈↓∧D. PERMANENT EQUIPMENT     5,000                --               --
␈↓ ↓H␈↓∧   (2 Datamedia terminals)

␈↓ ↓H␈↓∧E. EXPENDABLE SUPPLIES     1,632.            1,730.           1,834.
␈↓ ↓H␈↓∧   & EQUIPMENT(e.g.,copying,
␈↓ ↓H␈↓∧   office supplies, postage,      
␈↓ ↓H␈↓∧   freight, consulting,
␈↓ ↓H␈↓∧   honoraria)

␈↓ ↓H␈↓∧F. TRAVEL                  1,840.            1,950.           2,067.
␈↓ ↓H␈↓∧   All Domestic Travel

␈↓ ↓H␈↓∧G. PUBLICATIONS            1,000.            1,060.           1,124.

␈↓ ↓H␈↓∧H. OTHER COSTS             6,640.            7,038.           7,460.
␈↓ ↓H␈↓∧   1.Communication  1,600.
␈↓ ↓H␈↓∧     (telephone)     
␈↓ ↓H␈↓∧   2. Computer      5,040.
␈↓ ↓H␈↓∧      Equip. Maint.
␈↓ ↓H␈↓∧                          _______          ________          _______  

␈↓ ↓H␈↓∧I. TOTAL COSTS             68,416.          69,803.          75,631.
␈↓ ↓H␈↓∧    (A through H)

␈↓ ↓H␈↓∧J. INDIRECT COSTS:58% of   36,781.          40,486.          43,866.
␈↓ ↓H␈↓∧   A through H, less D.   ________         ________         ________     


␈↓ ↓H␈↓∧K. TOTAL COSTS            105,197.         110,289.         119,497.

␈↓ ↓H␈↓∧L. THREE YEAR TOTAL                                         334,983.
␈↓ ↓H␈↓α␈↓ εP␈↓ @11


␈↓ ↓H␈↓α␈↓ β7References                                ␈↓ εh␈↓xxx replace by reference to Moore thesis
                                          ␈↓ εh␈↓␈↓ π_␈↓αMoore, Robert C.␈↓ (1977) Reasoning about
␈↓ ↓H␈↓␈↓αBoyer, R.S., and Moore, J.S.␈↓ (1975) Proving␈↓ εh␈↓␈↓ π_Knowledge and Action, ␈↓↓1977 IJCAI
␈↓ ↓H␈↓␈↓ ↓xTheorems About LISP Functions, JACM       ␈↓ εh␈↓↓␈↓ π_Proceedings␈↓.  Available as <Arpanet:SAIL>
␈↓ ↓H␈↓␈↓ ↓xVol 22. No. 1 pp. 129-144. New York:      ␈↓ εh␈↓␈↓ π_IJCAI.PUB[1,RCM].
␈↓ ↓H␈↓␈↓ ↓xACM.
                                          ␈↓ εh␈↓␈↓αSato, M.␈↓ (1977) A study of Kripke-type Models
␈↓ ↓H␈↓␈↓αFilman, R.E.␈↓ (1979) The Interaction of    ␈↓ εh␈↓␈↓ π_for some Model Logics by Gentzen's
␈↓ ↓H␈↓␈↓ ↓xObservation and Inference.                ␈↓ εh␈↓␈↓ π_Sequential Method, (to appear in Publ.
␈↓ ↓H␈↓␈↓ ↓x(Stanford AI Memo AIM-327) Stanford       ␈↓ εh␈↓␈↓ π_R.I.M.S., Kyoto University).
␈↓ ↓H␈↓␈↓ ↓xUniversity.
                                          ␈↓ εh␈↓␈↓αWagner, Todd J.␈↓ (1977) Hardware Veri␈↓α␈↓βC␈↓α␈↓cation.
␈↓ ↓H␈↓␈↓αMcCarthy, J. and Painter, J.␈↓ (1967) Correctness␈↓ εh␈↓␈↓ π_Ph.D. thesis, Stanford University.
␈↓ ↓H␈↓␈↓ ↓xof a Compiler for Arithmetic Expressions. ␈↓ εh␈↓␈↓ π_Available as <Arpanet:SAIL>
␈↓ ↓H␈↓␈↓ ↓x␈↓↓Proc. Symposia in Applied Math., Math.    ␈↓ εh␈↓␈↓ π_THESIS.PUB[THE,TJW].
␈↓ ↓H␈↓↓␈↓ ↓xAspects of Computer Science␈↓ New York:
␈↓ ↓H␈↓␈↓ ↓xAmer. Math. Soc..                         ␈↓ εh␈↓␈↓αWeyhrauch, R. W., and Milner, R.␈↓ (1972)
                                          ␈↓ εh␈↓␈↓ π_Program Semanantics and Correctness in a
␈↓ ↓H␈↓␈↓αMcCarthy, J. and Hayes, P.J.␈↓ (1969) Some  ␈↓ εh␈↓␈↓ π_Mechanized Logic.  ␈↓↓First USA - Japan
␈↓ ↓H␈↓␈↓ ↓xPhilosophical Problems from the           ␈↓ εh␈↓↓␈↓ π_Computer Conference Proceedings.␈↓ Tokyo:
␈↓ ↓H␈↓␈↓ ↓xStandpoint of Arti␈↓α␈↓βC␈↓α␈↓cial Intelligence.     ␈↓ εh␈↓␈↓ π_Hitachi Priniting Company.
␈↓ ↓H␈↓␈↓ ↓x␈↓↓Machine Intelligence 4␈↓, pp. 463-502 (eds
␈↓ ↓H␈↓␈↓ ↓xMeltzer, B. and Michie, D.). Edinburgh:   ␈↓ εh␈↓␈↓αWeyhrauch, R. W.␈↓ (1977a) A Users Manual for
␈↓ ↓H␈↓␈↓ ↓xEdinburgh University Press.               ␈↓ εh␈↓␈↓ π_FOL. Stanford: Stanford AI Memo
                                          ␈↓ εh␈↓␈↓ π_AIM-235.1.  Available as <Arpanet:SAIL>
␈↓ ↓H␈↓␈↓αMcCarthy, J.␈↓ (1980) Circumscription - A Form␈↓ εh␈↓␈↓ π_FOLMAN.PUB[DOC,RWW].
␈↓ ↓H␈↓␈↓ ↓xof Non-Monotonic Reasoning.  ␈↓↓Arti␈↓␈↓βS␈↓␈↓↓cial
␈↓ ↓H␈↓↓␈↓ ↓xIntelligence␈↓, Volume l3, Numbers l, 2, April.␈↓ εh␈↓␈↓αWeyhrauch, R. W. (ed.)␈↓ (1977b) A Collection of
                                          ␈↓ εh␈↓␈↓ π_FOL Proofs (to be published).
␈↓ ↓H␈↓␈↓αMcCarthy, J.␈↓ (1977) First Order Theories of
␈↓ ↓H␈↓␈↓ ↓xIndividual Concepts and Propositions.
␈↓ ↓H␈↓␈↓ ↓x␈↓↓DMachine Intelligence 9␈↓, (Ed., Michie, D.).
␈↓ ↓H␈↓␈↓ ↓xEdinburgh, Edinburgh University Press.

␈↓ ↓H␈↓␈↓αMcCarthy, J.␈↓ (1979) Ascribing Mental Qualities
␈↓ ↓H␈↓␈↓ ↓xto Machines.  ␈↓↓Philosophical Perspectives in
␈↓ ↓H␈↓↓␈↓ ↓xArti␈↓␈↓βS␈↓␈↓↓cial Intelligence␈↓, (Ed., Ringle, M.).
␈↓ ↓H␈↓␈↓ ↓xHarvester Press.

␈↓ ↓H␈↓␈↓αCartwright, Robert and McCarthy, John␈↓
␈↓ ↓H␈↓␈↓ ↓x(1979) Recursive Programs as     Functions
␈↓ ↓H␈↓␈↓ ↓xin a First Order Theory. ␈↓↓Proceedings of the
␈↓ ↓H␈↓↓␈↓ ↓xInternational Conference on Mathematical
␈↓ ↓H␈↓↓␈↓ ↓xStudies of Information Processing␈↓, Kyoto,
␈↓ ↓H␈↓␈↓ ↓xJapan.

␈↓ ↓H␈↓␈↓αMcCarthy, J., Sato, M., Hayashi, T. and
␈↓ ↓H␈↓α␈↓ ↓xIgarashi, S.␈↓ (1977e) On the Model Theory
␈↓ ↓H␈↓␈↓ ↓xof Knowledge.  Presented at ␈↓↓IJCAI-1977␈↓;
␈↓ ↓H␈↓␈↓ ↓xto appear in the ␈↓↓SIGART Newsletter␈↓.